Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-04-28 06:56
f77211db
View on Github →
feat: drop completeness assumption in two integral lemmas (
#24428
)
Estimated changes
Modified
Mathlib/MeasureTheory/Integral/Bochner/ContinuousLinearMap.lean
modified
theorem
integral_const_mul_of_integrable
modified
theorem
integral_mul_const_of_integrable