isUnit_iff — Mathlib

English

An element is a unit iff its norm equals 1.

Русский

Элемент является единицей тогда и только тогда, когда его норма равна 1.

LaTeX

$$IsUnit(z) \iff \|z\| = 1$$

Lean4

theorem isUnit_iff {z : ℤ_[p]} : IsUnit z ↔ ‖z‖ = 1 :=
  ⟨fun h => by
    rcases isUnit_iff_dvd_one.1 h with ⟨w, eq⟩
    refine le_antisymm (norm_le_one _) ?_
    have := mul_le_mul_of_nonneg_left (norm_le_one w) (norm_nonneg z)
    rwa [mul_one, ← norm_mul, ← eq, norm_one] at this, fun h => ⟨⟨z, z.inv, mul_inv h, inv_mul h⟩, rfl⟩⟩

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