Revision #1280 → #2583 · back to history
modifiedTranslates map Borel sets to Borel sets5145e314d533
| Field | From #1280 | To #2583 |
|---|
| mathlib.decl | measurable_const_mul | MeasurableMul.measurable_const_mul |
| provenance | ai | ai-moderated |
modifiedHaar measure on the reals is Lebesgue measuredcd631dd9711
| Field | From #1280 | To #2583 |
|---|
| mathlib.decl | Real.isAddHaarMeasure_volume | instIsAddHaarMeasureVolume |
| provenance | ai | ai-moderated |
modifiedCartan's functional construction of Haar measure7672d5e17824
| Field | From #1280 | To #2583 |
|---|
| mathlib.decl | MeasureTheory.Measure.haarContent | MeasureTheory.Measure.haar.haarContent |
| provenance | ai | ai-moderated |
modifiedRelationship between left and right Haar measures via inversion2a00082dcbef
| Field | From #1280 | To #2583 |
|---|
| mathlib.decl | MeasureTheory.Measure.IsMulRightInvariant.inv | MeasureTheory.Measure.inv.instIsMulRightInvariant |
| provenance | ai | ai-moderated |
modifiedModular function (Haar modulus)7d03d7dc72af
| Field | From #1280 | To #2583 |
|---|
| mathlib.decl | MeasureTheory.modularCharacterFun | MeasureTheory.Measure.modularCharacterFun |
| provenance | ai | ai-moderated |
modifiedModular function is a continuous homomorphism15894486a13b
| Field | From #1280 | To #2583 |
|---|
| mathlib.decl | MeasureTheory.modularCharacter | MeasureTheory.Measure.modularCharacter |
| provenance | ai | ai-moderated |
modifiedExistence of semi-invariant measures on homogeneous spaces1fcb5550aa81
| Field | From #1280 | To #2583 |
|---|
| mathlib.decl | MeasureTheory.IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure | IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_HaarMeasure |
| provenance | ai | ai-moderated |