inner_mul_inner_add_areaForm_mul_areaForm

English

For any a, x, y ∈ E, the same bilinear relation holds in the two-argument form: ⟪a,x⟫⟪a,y⟫ + ω(a,x) ω(a,y) = ||a||^2 ⟪x,y⟫.

Русский

Для любых a, x, y ∈ E выполняется та же билинейная тождество: ⟪a,x⟫⟪a,y⟫ + ω(a,x) ω(a,y) = ||a||^2 ⟪x,y⟫.

LaTeX

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

Lean4

/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`. -/
theorem inner_mul_inner_add_areaForm_mul_areaForm (a x y : E) : ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫ :=
  congr_arg (fun f : E →ₗ[ℝ] ℝ => f y) (o.inner_mul_inner_add_areaForm_mul_areaForm' a x)

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