units_natAbs — Mathlib

English

For every unit u in the integer units ℤˣ, the natural absolute value natAbs u equals 1.

Русский

Для любой единицы u в группе единиц ℤˣ натуральная абсолютная величина natAbs u равна 1.

LaTeX

$$$ \operatorname{natAbs}(u) = 1 \quad\text{for all } u \in \mathbb{Z}^{\times}$$$

Lean4

theorem units_natAbs (u : ℤˣ) : natAbs u = 1 :=
  Units.ext_iff.1 <|
    Nat.units_eq_one
      ⟨natAbs u, natAbs ↑u⁻¹, by rw [← natAbs_mul, Units.mul_inv]; rfl, by rw [← natAbs_mul, Units.inv_mul]; rfl⟩

Похожие утверждения