Theorem MeasureTheory.Content.is_mul_left_invariant_outerMeasure

Modification history

2026-03-13 18:00
Mathlib/MeasureTheory/Measure/Content.lean
feat: generalize some `ContinuousMul` hypotheses to `SeparatelyContinuousMul` (#36562) …
Modified MeasureTheory.Content.is_mul_left_invariant_outerMeasureView on Github →
2025-04-09 09:39
Mathlib/MeasureTheory/Measure/Content.lean
feat: generalize Mathlib.MeasureTheory (#23147) …
Modified MeasureTheory.Content.is_mul_left_invariant_outerMeasureView on Github →
2025-02-16 15:19
Mathlib/MeasureTheory/Measure/Content.lean
chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)
Modified MeasureTheory.Content.is_mul_left_invariant_outerMeasureView on Github →
2023-05-22 18:01
Mathlib/MeasureTheory/Measure/Content.lean
feat: port MeasureTheory.Measure.Content (#4198)
Added MeasureTheory.Content.is_mul_left_invariant_outerMeasureView on Github →