Commit 2024-08-30 16:41 37b3e83b

View on Github →

chore(Group/Measure): drop a T2Space assumption (#16284)

Estimated changes

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

deleted theorem ContinuousLinearEquiv.isAddHaarMeasure_map

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