Theorem CircleIntegrable.const_fun_smul

Modification history

2026-08-06 00:12
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
feat: tag circle integrability as fun_prop (#41225) …
Deleted CircleIntegrable.const_fun_smulView on Github →
2025-07-03 05:41
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
feat: simple lemmas on circle integrability (#26618) …
Added CircleIntegrable.const_fun_smulView on Github →