Theorems · Theorem · measure theory

AlternatingMap.measure_def

∀ {G : Type u_4} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] [inst_2 : MeasurableSpace G]
  [inst_3 : BorelSpace G] [inst_4 : FiniteDimensional ℝ G] {n : ℕ} [_i : Fact (Module.finrank ℝ G = n)]
  (ω : G [⋀^Fin n]→ₗ[ℝ] ℝ),
  ω.measure = ‖ω ⇑(Module.finBasisOfFinrankEq ℝ G ⋯)‖₊ • (Module.finBasisOfFinrankEq ℝ G ⋯).addHaar

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpaceFiniteDimensionalFact