Mathlib Changelog
v4
Changelog
About
Github
Theorem
Real.circleAverage_eq_integral_add
Modification history
2025-05-12 19:50
Mathlib/MeasureTheory/Integral/CircleAverage.lean
chore: tidy various files (#24803)
Modified
Real.circleAverage_eq_integral_add
View on Github →
2025-05-09 13:13
Mathlib/MeasureTheory/Integral/CircleAverage.lean
feat: add circle averages (#24427) …
Added
Real.circleAverage_eq_integral_add
View on Github →