Documentation

Mathlib.Data.Fintype.Units

fintype instances relating to units #

Equations
@[simp]
theorem UnitsInt.univ :
Finset.univ = {1, -1}
instance instFintypeUnitsOfDecidableEq {α : Type u_1} [Monoid α] [Fintype α] [DecidableEq α] :
Equations
instance instFiniteUnits {α : Type u_1} [Monoid α] [Finite α] :
Equations
  • =