Documentation

Mathlib.Algebra.Group.Nat.Units

The unit of the natural numbers #

Units #

source
theorem Nat.units_eq_one (u : ℕˣ) :
u = 1
source
theorem Nat.addUnits_eq_zero (u : AddUnits ℕ) :
u = 0
source
instance Nat.unique_units :
Unique ℕˣ
Equations
    source
    instance Nat.unique_addUnits :
    Unique (AddUnits ℕ)
    Equations
      source
      theorem Nat.isUnit_iff {n : ℕ} :
      IsUnit n ↔ n = 1

      Alias of isUnit_iff_eq_one for discoverability.

      source
      theorem Nat.isAddUnit_iff {n : ℕ} :
      IsAddUnit n ↔ n = 0

      Alias of isAddUnit_iff_eq_zero for discoverability.