Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-05 06:48
00335dd9
View on Github →
feat: multiplying by a constant on the right preserves integrability (
#27948
)
Estimated changes
Modified
Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
added
theorem
MeasureTheory.MemLp.mul_const