inner_mul_inner_add_areaForm_mul_areaForm'

English

For any a, x, y in E, the cross-term identity holds: ⟪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⟫`. (See
`Orientation.inner_mul_inner_add_areaForm_mul_areaForm` for the "applied" form.) -/
theorem inner_mul_inner_add_areaForm_mul_areaForm' (a x : E) :
    ⟪a, x⟫ • innerₛₗ ℝ a + ω a x • ω a = ‖a‖ ^ 2 • innerₛₗ ℝ x :=
  by
  by_cases ha : a = 0
  · simp [ha]
  apply (o.basisRightAngleRotation a ha).ext
  intro i
  fin_cases i
  · simp [real_inner_self_eq_norm_sq, mul_comm, real_inner_comm]
  · simp [real_inner_self_eq_norm_sq, mul_comm, o.areaForm_swap a x]

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