Theorems · Definition · functional analysis

Orientation.volumeForm

{E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      {n : ℕ} → [_i : Fact (Module.finrank ℝ E = n)] → Orientation ℝ E (Fin n) → E [⋀^Fin n]→ₗ[ℝ] ℝ

The volume form on an oriented real inner product space, a nonvanishing top-dimensional alternating form uniquely defined by compatibility with the orientation and inner product structure.

Defined in

Mathlib.Analysis.InnerProductSpace.Orientation

Cited by

24 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceFact