Commit 2025-03-23 01:47 69b18d4c

View on Github →

golf: use #22273 more (#23011)

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

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

modified theorem MeasureTheory.Measure.haar.index_empty