fintype instances relating to units

instance UnitsInt.fintype : Fintype ℤˣ

Equations

• UnitsInt.fintype = { elems := {1, -1}, complete := UnitsInt.fintype.proof_1 }

@[simp]

theorem UnitsInt.univ : Finset.univ = {1, -1}

@[simp]

theorem Fintype.card_units_int : Fintype.card ℤˣ = 2

instance instFintypeUnitsOfDecidableEq {α : Type u_1} [Monoid α] [Fintype α] [DecidableEq α] : Fintype αˣ

Equations

• instFintypeUnitsOfDecidableEq = Fintype.ofEquiv { p : α × α // p.1 * p.2 = 1 ∧ p.2 * p.1 = 1 } (unitsEquivProdSubtype α).symm

instance instFiniteUnits {α : Type u_1} [Monoid α] [Finite α] : Finite αˣ

Equations

• ⋯ = ⋯

theorem Nat.card_units (α : Type u_1) [GroupWithZero α] : Nat.card αˣ = Nat.card α - 1

theorem Nat.card_eq_card_units_add_one (α : Type u_1) [GroupWithZero α] [Finite α] : Nat.card α = Nat.card αˣ + 1

theorem Fintype.card_units (α : Type u_1) [GroupWithZero α] [Fintype α] [DecidableEq α] : Fintype.card αˣ = Fintype.card α - 1

theorem Fintype.card_eq_card_units_add_one (α : Type u_1) [GroupWithZero α] [Fintype α] [DecidableEq α] : Fintype.card α = Fintype.card αˣ + 1