Documentation

Mathlib.Data.Fintype.Units

fintype instances relating to units #

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