mathlib3 documentation

data.nat.units

The units of the natural numbers as a monoid and add_monoid #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
theorem nat.units_eq_one (u : ℕˣ) :
u = 1
source
theorem nat.add_units_eq_zero (u : add_units ℕ) :
u = 0
source
@[protected, simp]
theorem nat.is_unit_iff {n : ℕ} :
is_unit n ↔ n = 1
source
@[protected, instance]
def nat.unique_units  :
unique ℕˣ
Equations
source
@[protected, instance]
def nat.unique_add_units  :
unique (add_units ℕ)
Equations