Theorem CircleIntegrable.fun_sum

Modification history

2026-08-06 00:12
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
feat: tag circle integrability as fun_prop (#41225) …
Deleted CircleIntegrable.fun_sumView on Github →
2025-11-24 08:57
Mathlib/MeasureTheory/Integral/CircleIntegral.lean
feat: behavior of the proximity function under addition (#31556) …
Added CircleIntegrable.fun_sumView on Github →