Theorems · Theorem · geometry

Orientation.inner_mul_inner_add_areaForm_mul_areaForm

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (a x y : E),
  inner ℝ a x * inner ℝ a y + (o.areaForm a) x * (o.areaForm a) y = ‖a‖ ^ 2 * inner ℝ x y

For vectors a x y : E, the identity ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫.

Defined in

Mathlib.Analysis.InnerProductSpace.TwoDim

Cited by

2 results in Mathlib

Foundations

Depth 271 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFact