Theorems · Theorem · functional analysis

Orientation.abs_volumeForm_apply_of_pairwise_orthogonal

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) {v : Fin n → E},
  (Pairwise fun i j => inner ℝ (v i) (v j) = 0) → |o.volumeForm v| = ∏ i, ‖v i‖

Let v be an indexed family of n orthogonal vectors in an oriented n-dimensional real inner product space E. The output of the volume form of E when evaluated on v is, up to sign, the product of the norms of the vectors v i.

Defined in

Mathlib.Analysis.InnerProductSpace.Orientation

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact