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 instFintypeUnits {α : Type u_1} [Monoid α] [Fintype α] [DecidableEq α] : Fintype αˣ

Equations

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

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

Equations

• (_ : Finite αˣ) = (_ : Finite αˣ)

theorem Fintype.card_eq_card_units_add_one {α : Type u_1} [GroupWithZero α] [Fintype α] [DecidableEq α] : Fintype.card α = Fintype.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