fintype instances relating to units #
theorem
Fintype.card_eq_card_units_add_one
{α : Type u_1}
[GroupWithZero α]
[Fintype α]
[DecidableEq α]
:
Fintype.card α = Fintype.card αˣ + 1
theorem
Fintype.card_units
{α : Type u_1}
[GroupWithZero α]
[Fintype α]
[DecidableEq α]
:
Fintype.card αˣ = Fintype.card α - 1