Documentation

Mathlib.Data.Fintype.Units

fintype instances relating to units #

Equations
@[simp]
theorem UnitsInt.univ :
Finset.univ = {1, -1}
instance instFintypeUnits {α : Type u_1} [inst : Monoid α] [inst : Fintype α] [inst : DecidableEq α] :
Equations
instance instFiniteUnits {α : Type u_1} [inst : Monoid α] [inst : Finite α] :
Equations
theorem Fintype.card_units {α : Type u_1} [inst : GroupWithZero α] [inst : Fintype α] [inst : Fintype αˣ] :