Theorems · Theorem · measure theory

MeasureTheory.volume_eq_of_finrank_eq_one

∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : MeasurableSpace E]
  [inst_3 : BorelSpace E] [inst_4 : FiniteDimensional ℝ E],
  Module.finrank ℝ E = 1 →
    ∀ {v : E}, v ≠ 0 → MeasureTheory.volume = ‖v‖ₑ • MeasureTheory.Measure.map (fun x => x • v) MeasureTheory.volume

Volume on a 1-dimensional real vector space is equivalent to a scaled volume on ℝ.

Defined in

Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceMeasurableSpaceBorelSpaceFiniteDimensional