Theorems · Theorem · measure theory

MeasureTheory.Measure.addHaar_parallelepiped

∀ {ι : Type u_2} {G : Type u_3} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : NormedAddCommGroup G]
  [inst_3 : NormedSpace ℝ G] [inst_4 : MeasurableSpace G] [inst_5 : BorelSpace G] (b : Module.Basis ι ℝ G) (v : ι → G),
  b.addHaar (parallelepiped v) = ENNReal.ofReal |b.det v|

Defined in

Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeDecidableEqNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpace