normSq_kahler — Mathlib

English

The squared magnitude of kahler equals the product of the squared norms: Complex.normSq(kahler(x,y)) = ||x||^2 ||y||^2.

Русский

Квадрат модуля kahler равен произведению квадратов норм: Complex.normSq(kahler(x,y)) = ||x||^2 ||y||^2.

LaTeX

$$Complex.normSq\\big(o.kahler x y\\big) = \\|x\\|^2 \\|y\\|^2$$

Lean4

theorem normSq_kahler (x y : E) : Complex.normSq (o.kahler x y) = ‖x‖ ^ 2 * ‖y‖ ^ 2 := by
  simpa [kahler_apply_apply, Complex.normSq, sq] using o.inner_sq_add_areaForm_sq x y

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