norm_eq_one_iff' — Mathlib

English

For hd ≤ 0 and z ∈ Z√d, z.norm = 1 iff z is a unit.

Русский

Если $d \\le 0$ и $z \\in \\mathbb{Z}[\\sqrt{d}]$, то $\\|z\\| = 1$ тогда и только тогда, когда $z$ — единица.

LaTeX

$${d : Int} (hd : d ≤ 0) (z : ℤ√d) : z.norm = 1 ↔ IsUnit z$$

Lean4

theorem norm_eq_one_iff' {d : ℤ} (hd : d ≤ 0) (z : ℤ√d) : z.norm = 1 ↔ IsUnit z := by
  rw [← norm_eq_one_iff, ← Int.natCast_inj, Int.natAbs_of_nonneg (norm_nonneg hd z), Int.ofNat_one]

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