norm_kahler — Mathlib

English

The norm of kahler equals the product of the norms of the arguments: ||o.kahler x y|| = ||x|| · ||y||.

Русский

Норма kahler равна произведению норм аргументов: ||o.kahler x y|| = ||x|| · ||y||.

LaTeX

$$||o.kahler x y|| = ||x|| \\cdot ||y||$$

Lean4

theorem norm_kahler (x y : E) : ‖o.kahler x y‖ = ‖x‖ * ‖y‖ :=
  by
  rw [← sq_eq_sq₀, Complex.sq_norm]
  · linear_combination o.normSq_kahler x y
  · positivity
  · positivity

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