Mathlib Map

Theorems · Theorem · measure theory

Module.Basis.addHaar_def

∀ {ι : Type u_5} {E : Type u_6} [inst : Fintype ι] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] (b : Module.Basis ι ℝ E),
  b.addHaar = MeasureTheory.Measure.addHaarMeasure b.parallelepiped
Defined in
Mathlib.MeasureTheory.Measure.Haar.OfBasis
Cited by
7 results in Mathlib
Foundations
Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
FintypeNormedAddCommGroupNormedSpaceMeasurableSpaceBorelSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Module.Basis.addHaar_eq_iff · cited by 5Basis.addHaar_eq_iffEuclideanSpace.volume_preserving_symm_measurableEquiv_toLp · cited by 4EuclideanSpace.volume_pre…Module.Basis.addHaar_self · cited by 3Basis.addHaar_selfComplex.volume_preserving_equiv_pi · cited by 2Complex.volume_preserving…Real.volume_eq_stieltjes_id · cited by 1Real.volume_eq_stieltjes_…Orientation.measure_eq_volume · cited by 1Orientation.measure_eq_vo…Module.Basis.addHaar_reindex · cited by 0Basis.addHaar_reindexReal · cited by 25697RealNormedAddCommGroup · cited by 15752NormedAddCommGroupMeasurableSpace · cited by 13106MeasurableSpaceNormedSpace · cited by 12499NormedSpaceMeasureTheory.Measure · cited by 10939MeasureTheory.MeasureFintype · cited by 7736FintypeBorelSpace · cited by 1602BorelSpaceModule.Basis · cited by 1477Module.BasisMeasureTheory.Measure.addHaarMeasure · cited by 21Measure.addHaarMeasureModule.Basis.addHaar · cited by 15Basis.addHaarModule.Basis.parallelepiped · cited by 12Basis.parallelepipedBasis.addHaar_defCITED BYCITES

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by7

Results whose statement or proof uses this declaration.