norm_mul — Mathlib

English

The norm is multiplicative over complex multiplication: ‖z w‖ = ‖z‖ ‖w‖.

Русский

Норма умножения комплексных чисел дзелится на произведение норм: ‖z w‖ = ‖z‖ ‖w‖.

LaTeX

$$$\forall z,w \in \mathbb{C},\; \|z w\| = \|z\| \|w\|$$$

Lean4

@[simp 1100]
protected theorem norm_mul (z w : ℂ) : ‖z * w‖ = ‖z‖ * ‖w‖ := by
  rw [norm_def, norm_def, norm_def, normSq_mul, Real.sqrt_mul (normSq_nonneg _)]

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