Theorems · Definition · measure theory

Module.Basis.addHaar

{ι : Type u_5} →
  {E : Type u_6} →
    [Fintype ι] →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedSpace ℝ E] →
          [inst_2 : MeasurableSpace E] → [BorelSpace E] → Module.Basis ι ℝ E → MeasureTheory.Measure E

The Lebesgue measure associated to a basis, giving measure 1 to the parallelepiped spanned by the basis.

Defined in

Mathlib.MeasureTheory.Measure.Haar.OfBasis

Cited by

15 results in Mathlib

Foundations

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

Assumes

FintypeNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpace