normMonoidHom — Mathlib

English

The map x ↦ norm(x) is a monoid homomorphism from Z[√d] to Z.

Русский

Отображение $x \\mapsto \\operatorname{norm}(x)$ является гомоморфизмом моноидов от $\\mathbb{Z}[\\sqrt{d}]$ к $\\mathbb{Z}$.

LaTeX

$$$\\operatorname{normMonoidHom} : \\mathbb{Z}\\!\\sqrt{d} \\to^* \\mathbb{Z}$ with \\operatorname{norm}(xy) = \\operatorname{norm}(x) \\operatorname{norm}(y) \\text{ and } \\operatorname{norm}(1)=1$$$

Lean4

/-- `norm` as a `MonoidHom`. -/
def normMonoidHom : ℤ√d →* ℤ where
  toFun := norm
  map_mul' := norm_mul
  map_one' := norm_one

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