Theorems · Theorem · functional analysis

Orientation.volumeForm_robust

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (b : OrthonormalBasis (Fin n) ℝ E),
  b.toBasis.orientation = o → o.volumeForm = b.toBasis.det

The volume form on an oriented real inner product space can be evaluated as the determinant with respect to any orthonormal basis of the space compatible with the orientation.

Defined in

Mathlib.Analysis.InnerProductSpace.Orientation

Cited by

4 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact