fintype instances relating to units

ink

instance UnitsInt.fintype : Fintype ℤˣ

Equations

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

Equations

• instFintypeUnits = Fintype.ofEquiv { p // p.fst * p.snd = 1 ∧ p.snd * p.fst = 1 } (Equiv.symm (unitsEquivProdSubtype α))

ink

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

Equations

• @instFiniteUnits = @instFiniteUnits.proof_1

ink

theorem Fintype.card_units {α : Type u_1} [inst : GroupWithZero α] [inst : Fintype α] [inst : Fintype αˣ] : Fintype.card αˣ = Fintype.card α - 1