Documentation

Mathlib.Data.Fintype.Units

fintype instances relating to units #

source
instance UnitsInt.fintype :
Fintype ℤˣ
Equations
    source
    @[simp]
    theorem UnitsInt.univ :
    Finset.univ = {1, -1}
    source
    @[simp]
    theorem Fintype.card_units_int :
    card ℤˣ = 2
    source
    instance instFintypeUnitsOfDecidableEq {α : Type u_1} [Monoid α] [Fintype α] [DecidableEq α] :
    Fintype αˣ
    Equations
      source
      instance instFiniteUnits {α : Type u_1} [Monoid α] [Finite α] :
      Finite αˣ
      source
      theorem Nat.card_units (α : Type u_1) [GroupWithZero α] :
      Nat.card αˣ = Nat.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 α] :
      card αˣ = card α - 1
      source
      theorem Fintype.card_eq_card_units_add_one (α : Type u_1) [GroupWithZero α] [Fintype α] [DecidableEq α] :
      card α = card αˣ + 1