mathlib3 documentation

data.fintype.units

fintype instances relating to units #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
Equations
@[simp]
theorem units_int.univ  :
finset.univ = {1, -1}
@[protected, instance]
def units.fintype {α : Type u_1} [monoid α] [fintype α] [decidable_eq α] :
Equations
@[protected, instance]
def units.finite {α : Type u_1} [monoid α] [finite α] :