Theorem Complex.dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleO

Modification history

2026-01-06 22:13
Mathlib/Analysis/Complex/Schwarz.lean
feat(Schwarz): add a version for maps with derivative zero (#33563) …
Added Complex.dist_le_mul_div_pow_of_mapsTo_ball_of_isLittleOView on Github →