The unit of the natural numbers

Units

theorem Nat.units_eq_one (u : ℕˣ) : u = 1

theorem Nat.addUnits_eq_zero (u : AddUnits ℕ) : u = 0

instance Nat.unique_units : Unique ℕˣ

Equations

• Nat.unique_units = { default := 1, uniq := Nat.units_eq_one }

instance Nat.unique_addUnits : Unique (AddUnits ℕ)

Equations

• Nat.unique_addUnits = { default := 0, uniq := Nat.addUnits_eq_zero }

theorem Nat.isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1

Alias of isUnit_iff_eq_one for discoverability.

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

Alias of isAddUnit_iff_eq_zero for discoverability.