The additive Haar measure of the standard basis

The additive Haar measure attached to a basis gives measure one to the parallelepiped the basis spans. For the standard basis of ι → ℝ that parallelepiped is the unit cube, so the measure is product Lebesgue measure.

Main results

• Module.Basis.addHaar_basisFun — the additive Haar measure of Pi.basisFun ℝ ι is volume.

theorem Module.Basis.addHaar_basisFun (ι : Type u_1) [Fintype ι] : (Pi.basisFun ℝ ι).addHaar = MeasureTheory.volume

The additive Haar measure attached to the standard basis of ι → ℝ is product Lebesgue measure, because the basis parallelepiped is the unit cube.