inner_sq_add_areaForm_sq — Mathlib

English

The sum of the squares of the inner product and the area form equals the product of norms: ⟪a,b⟫^2 + ω(a,b)^2 = ||a||^2 ||b||^2 for all a,b ∈ E.

Русский

Сумма квадратов внутреннего произведения и формы площади равна произведению норм: ⟪a,b⟫^2 + ω(a,b)^2 = ||a||^2 ||b||^2 для всех a,b ∈ E.

LaTeX

$$$\\langle a,b\\rangle^2 + \\omega(a,b)^2 = \\|a\\|^2 \\|b\\|^2$$$

Lean4

theorem inner_sq_add_areaForm_sq (a b : E) : ⟪a, b⟫ ^ 2 + ω a b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2 := by
  simpa [sq, real_inner_self_eq_norm_sq] using o.inner_mul_inner_add_areaForm_mul_areaForm a b b

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