Mathlib Changelog
v4
Changelog
About
Github
Theorem
norm_torusIntegral_le_of_norm_le_const
Modification history
2023-06-12 04:10
Mathlib/MeasureTheory/Integral/TorusIntegral.lean
feat: port MeasureTheory.Integral.TorusIntegral (#4942)
Added
norm_torusIntegral_le_of_norm_le_const
View on Github →