norm_eq_of_associated — Mathlib

English

If x and y are associated in Z√d, then x.norm = y.norm.

Русский

Если $x$ и $y$ ассоциированы в $\\mathbb{Z}[\\sqrt{d}]$, то их нормы равны.

LaTeX

$${d : Int} (hd : d ≤ 0) {x y : ℤ√d} (h : Associated x y) : x.norm = y.norm$$

Lean4

theorem norm_eq_of_associated {d : ℤ} (hd : d ≤ 0) {x y : ℤ√d} (h : Associated x y) : x.norm = y.norm :=
  by
  obtain ⟨u, rfl⟩ := h
  rw [norm_mul, (norm_eq_one_iff' hd _).mpr u.isUnit, mul_one]

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