Fintype.card_units

theorem Fintype.card_units : ∀ {α : Type u_1} [inst : GroupWithZero α] [inst_1 : Fintype α] [inst_2 : DecidableEq α], Fintype.card αˣ = Fintype.card α - 1

This theorem, `Fintype.card_units`, states that for any type `α` which is equipped with a group with zero structure (denoted as `GroupWithZero α`), given that `α` has a finite number of distinct elements (denoted as `Fintype α`), and the equality between elements of `α` is decidable (`DecidableEq α`), the number of units in `α` (denoted as `αˣ`, where a unit is an element with a multiplicative inverse) is equal to the total number of elements in `α` subtracted by one (`Fintype.card α - 1`). Essentially, it defines how to determine the number of invertible elements in any finite group with a zero element.

More concisely: In a finite group with zero element, the number of units (invertible elements) equals the total number of elements minus one.