Commit 2024-07-25 11:52 918e1fbc
View on Github →feat(Group/Measure): drop a MeasurableMul assumption (#15041)
In fact, for μ ≠ 0 the definition still implies that the multiplication is (a.e.) measurable,
but Lean doesn't have to search for this instance now.