norm_div — Mathlib

English

The norm respects division: ‖z / w‖ = ‖z‖ / ‖w‖ for z,w ∈ ℂ with w ≠ 0.

Русский

Норма сохраняет деление: ‖z / w‖ = ‖z‖ / ‖w‖ при w ≠ 0.

LaTeX

$$$\forall z,w \in \mathbb{C},\; w \neq 0 \Rightarrow \|\tfrac{z}{w}\| = \tfrac{\|z\|}{\|w\|}$$$

Lean4

@[simp 1100]
protected theorem norm_div (z w : ℂ) : ‖z / w‖ = ‖z‖ / ‖w‖ := by
  rw [norm_def, norm_def, norm_def, normSq_div, Real.sqrt_div (normSq_nonneg _)]

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