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.

source
@[protected, instance]
def units_int.fintype  :
fintype ℤˣ
Equations
source
@[simp]
theorem units_int.univ  :
finset.univ = {1, -1}
source
@[simp]
theorem fintype.card_units_int  :
fintype.card ℤˣ = 2
source
@[protected, instance]
def units.fintype {α : Type u_1} [monoid α] [fintype α] [decidable_eq α] :
fintype αˣ
Equations
source
@[protected, instance]
def units.finite {α : Type u_1} [monoid α] [finite α] :
finite αˣ
source
theorem fintype.card_units {α : Type u_1} [group_with_zero α] [fintype α] [fintype αˣ] :
fintype.card αˣ = fintype.card α - 1