Documentation

Mathlib.Data.Fintype.Units

fintype instances relating to units #

source
instance UnitsInt.fintype :
Fintype ℤˣ
source
@[simp]
theorem UnitsInt.univ :
Finset.univ = {1, -1}
source
@[simp]
theorem Fintype.card_units_int :
Fintype.card ℤˣ = 2
source
instance instFintypeUnits {α : Type u_1} [Monoid α] [Fintype α] [DecidableEq α] :
Fintype αˣ
source
instance instFiniteUnits {α : Type u_1} [Monoid α] [Finite α] :
Finite αˣ
source
theorem Fintype.card_eq_card_units_add_one {α : Type u_1} [GroupWithZero α] [Fintype α] [DecidableEq α] :
Fintype.card α = Fintype.card αˣ + 1
source
theorem Nat.card_eq_card_units_add_one {α : Type u_1} [GroupWithZero α] [Finite α] :
Nat.card α = Nat.card αˣ + 1
source
theorem Fintype.card_units {α : Type u_1} [GroupWithZero α] [Fintype α] [DecidableEq α] :
Fintype.card αˣ = Fintype.card α - 1