Theorem Real.circleAverage_mono

Modification history

2025-11-12 06:28
Mathlib/MeasureTheory/Integral/CircleAverage.lean
feat: behaviour of Nevanlinna functions under multiplication (#30494) …
Added Real.circleAverage_monoView on Github →