fintype instances relating to units #
Equations
- UnitsInt.fintype = { elems := {1, -1}, complete := UnitsInt.fintype.proof_1 }
instance
instFintypeUnits
{α : Type u_1}
[inst : Monoid α]
[inst : Fintype α]
[inst : DecidableEq α]
:
Equations
- instFintypeUnits = Fintype.ofEquiv { p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1 } (Equiv.symm (unitsEquivProdSubtype α))
Equations
theorem
Fintype.card_units
{α : Type u_1}
[inst : GroupWithZero α]
[inst : Fintype α]
[inst : Fintype αˣ]
:
Fintype.card αˣ = Fintype.card α - 1