Commit 2025-08-05 10:41 8a90bb86

View on Github →

feat: add mulEquivHaarChar (#25829) API for the positive real factor by which an continuous multiplicative equivalence scales a regular Haar measure on a locally compact topological group. From FLT.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

added theorem MeasureTheory.Measure.IsHaarMeasure.nnreal_smul

Created Mathlib/MeasureTheory/Measure/Haar/MulEquivHaarChar.lean

added theorem MeasureTheory.integral_comap_eq_mulEquivHaarChar_smul

added theorem MeasureTheory.mulEquivHaarChar_eq

added theorem MeasureTheory.mulEquivHaarChar_pos

added theorem MeasureTheory.mulEquivHaarChar_refl

added theorem MeasureTheory.mulEquivHaarChar_smul_eq_comap

added theorem MeasureTheory.mulEquivHaarChar_smul_integral_map

added theorem MeasureTheory.mulEquivHaarChar_smul_map

added theorem MeasureTheory.mulEquivHaarChar_smul_preimage

added theorem MeasureTheory.mulEquivHaarChar_trans

Modified Mathlib/MeasureTheory/Measure/Haar/Unique.lean

added theorem MeasureTheory.Measure.haarScalarFactor_smul_smul

added theorem MeasureTheory.Measure.mul_haarScalarFactor_smul