Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-08-16 00:24
462359db
View on Github →
feat(measure): prove Haar measure = Lebesgue measure on R (
#8639
)
Estimated changes
Created
src/measure_theory/measure/haar_lebesgue.lean
added
theorem
measure_theory.haar_measure_eq_lebesgue_measure
added
theorem
measure_theory.is_add_left_invariant_real_volume
added
def
topological_space.positive_compacts.Icc01