Mathlib.Algebra.Group.Nat.Units

Nat.units_eq_one theorem

(u : ℕˣ) : u = 1

Full source

lemma units_eq_one (u : ℕℕˣ) : u = 1 := Units.ext <| Nat.eq_one_of_dvd_one ⟨u.inv, u.val_inv.symm⟩

Multiplicative Units of Natural Numbers are Trivial

Informal description

For any multiplicative unit $u$ of the natural numbers, $u$ is equal to $1$.

Nat.addUnits_eq_zero theorem

(u : AddUnits ℕ) : u = 0

Full source

lemma addUnits_eq_zero (u : AddUnits ℕ) : u = 0 :=
  AddUnits.ext <| (Nat.eq_zero_of_add_eq_zero u.val_neg).1

Additive Units of Natural Numbers are Trivial

Informal description

For any additive unit $u$ of the natural numbers, $u$ is equal to $0$.

Nat.unique_units instance

: Unique ℕˣ

Full source

instance unique_units : Unique ℕℕˣ where
  default := 1
  uniq := Nat.units_eq_one

Uniqueness of Multiplicative Units in Natural Numbers

Informal description

The multiplicative units of the natural numbers form a unique type, with the only unit being $1$.

Nat.unique_addUnits instance

: Unique (AddUnits ℕ)

Full source

instance unique_addUnits : Unique (AddUnits ℕ) where
  default := 0
  uniq := Nat.addUnits_eq_zero

Uniqueness of Additive Units in Natural Numbers

Informal description

The additive units of the natural numbers form a unique type, with the only unit being $0$.

Nat.isUnit_iff theorem

{n : ℕ} : IsUnit n ↔ n = 1

Full source

/-- Alias of `isUnit_iff_eq_one` for discoverability. -/
protected lemma isUnit_iff {n : ℕ} : IsUnitIsUnit n ↔ n = 1 := isUnit_iff_eq_one

Characterization of Multiplicative Units in Natural Numbers: $n$ is a unit iff $n = 1$

Informal description

For any natural number $n$, $n$ is a multiplicative unit if and only if $n = 1$.

Nat.isAddUnit_iff theorem

{n : ℕ} : IsAddUnit n ↔ n = 0

Full source

/-- Alias of `isAddUnit_iff_eq_zero` for discoverability. -/
protected lemma isAddUnit_iff {n : ℕ} : IsAddUnitIsAddUnit n ↔ n = 0 := isAddUnit_iff_eq_zero

Characterization of Additive Units in Natural Numbers: $n$ is an additive unit iff $n = 0$

Informal description

For any natural number $n$, $n$ is an additive unit if and only if $n = 0$.