The units of the natural numbers as a Monoid and AddMonoid

ink

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

ink

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

ink

@[simp]

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

ink

instance Nat.unique_units : Unique ℕˣ

Equations

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

ink

instance Nat.unique_addUnits : Unique (AddUnits ℕ)

Equations

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