norm_mul — Mathlib

English

For any n,m in Z[√d], the norm of their product equals the product of their norms.

Русский

Для любых $n,m \\in \\mathbb{Z}[\\sqrt{d}]$ норма произведения равна произведению норм.

LaTeX

$$$\\operatorname{norm}(n m) = \\operatorname{norm}(n) \\operatorname{norm}(m)$, for all $n,m \\in \\mathbb{Z}\\sqrt{d}$$$

Lean4

@[simp]
theorem norm_mul (n m : ℤ√d) : norm (n * m) = norm n * norm m :=
  by
  simp only [norm, im_mul, re_mul]
  ring

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