The unit of the natural numbers

Units

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

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

@[simp]

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

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 }