Theorem TorusIntegrable.torusIntegrable_zero_radius

Modification history

2023-06-12 04:10
Mathlib/MeasureTheory/Integral/TorusIntegral.lean
feat: port MeasureTheory.Integral.TorusIntegral (#4942)
Added TorusIntegrable.torusIntegrable_zero_radiusView on Github →