Theorem MeasureTheory.measure_lt_top_of_isCompact_of_mulLeftInvariant'

Modification history

2023-06-04 05:44

Mathlib/MeasureTheory/Group/Measure.lean

style: recover `Is` of `Foo` which is ported from `is_foo` (#4639) …

Deleted MeasureTheory.measure_lt_top_of_isCompact_of_mulLeftInvariant'View on Github →

2023-05-30 10:47

Mathlib/MeasureTheory/Group/Measure.lean

feat: port MeasureTheory.Group.Measure (#4496)

Added MeasureTheory.measure_lt_top_of_isCompact_of_mulLeftInvariant'View on Github →