English
For any a,x ∈ E, the linear-functional identity holds: ⟪a,x⟫ ω(a) - ω(a,x) ⟪a,·⟫ = ||a||^2 ω(x,·).
Русский
Для любых a,x ∈ E верно тождество линейных функционалов: ⟪a,x⟫ ω(a) - ω(a,x) ⟪a,·⟫ = ||a||^2 ω(x,·).
LaTeX
$$$\\langle a,x\\rangle \\omega(a) - \\omega(a,x) \\langle a,\\cdot\\rangle = \\|a\\|^2 \\omega(x,\\cdot)$$
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_areaForm_sub` for the "applied" form.) -/
theorem inner_mul_areaForm_sub' (a x : E) : ⟪a, x⟫ • ω a - ω a x • innerₛₗ ℝ a = ‖a‖ ^ 2 • ω 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, o.areaForm_swap a x]
· simp [real_inner_self_eq_norm_sq, mul_comm, real_inner_comm]
