prod_norm_sq — Mathlib

English

The squared norm on the product equals the sum of squared norms of components: ∥(x,y)∥^2 = ∥x∥^2 + ∥y∥^2.

Русский

Квадрат нормы на произведении равен сумме квадратов компонент: ∥(x,y)∥^2 = ∥x∥^2 + ∥y∥^2.

LaTeX

$$$\\| (x,y) \\|^{2} = \\|x\\|^{2} + \\|y\\|^{2}$$$

Lean4

theorem prod_norm_sq (x : C⋆ᵐᵒᵈ(A, E × F)) : ‖x‖ ^ 2 = ‖⟪x.1, x.1⟫_A + ⟪x.2, x.2⟫_A‖ := by simp [prod_norm]

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