Theorem CircleIntegrable.const_smul

Modification history

2026-10-29 18:27
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
chore(MeasureTheory): generalize `CircleIntegrable.const_smul` (#45189) …
Modified CircleIntegrable.const_smulView on Github →
2025-07-03 05:41
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
feat: simple lemmas on circle integrability (#26618) …
Added CircleIntegrable.const_smulView on Github →