norm_eq_one_iff_mem_unitary — Mathlib

English

An element a of Z[√d] has norm equal to 1 if and only if it is a unitary element of the ring Z[√d].

Русский

Элемент a из Z[√d] имеет норму равную 1 тогда и только тогда, когда он является унитарным элементом кольца Z[√d].

LaTeX

$$$\\forall d\\in\\mathbb{Z},\\forall a\\in\\mathbb{Z}[\\sqrt{d}],\\; \\operatorname{norm}(a)=1\\iff a\\in\\mathrm{unitary}(\\mathbb{Z}[\\sqrt{d}]).$$$

Lean4

/-- An element of `ℤ√d` has norm equal to `1` if and only if it is contained in the submonoid
of unitary elements. -/
theorem norm_eq_one_iff_mem_unitary {d : ℤ} {a : ℤ√d} : a.norm = 1 ↔ a ∈ unitary (ℤ√d) :=
  by
  rw [unitary.mem_iff_self_mul_star, ← norm_eq_mul_conj]
  norm_cast

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