fintype instances relating to units

@[implicit_reducible]

instance UnitsInt.fintype : Fintype ℤˣ

@[simp]

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

@[simp]

theorem Fintype.card_units_int : card ℤˣ = 2

@[implicit_reducible]

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

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

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 α] : card αˣ = card α - 1

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