mker_norm_eq_unitary — Mathlib

English

The kernel of the norm map on Z[√d] equals the unitary submonoid of Z[√d].

Русский

Ядро отображения нормы на Z[√d] равно подмоноиду единичных элементов Z[√d].

LaTeX

$$$\\operatorname{mker}(\\text{normMonoidHom})=\\mathrm{unitary}(\\mathbb{Z}[\\sqrt{d}]).$$$

Lean4

/-- The kernel of the norm map on `ℤ√d` equals the submonoid of unitary elements. -/
theorem mker_norm_eq_unitary {d : ℤ} : MonoidHom.mker (@normMonoidHom d) = unitary (ℤ√d) :=
  Submonoid.ext fun _ => norm_eq_one_iff_mem_unitary

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