Commit 2026-01-03 17:21 60148e94

View on Github →

feat(Schwarz): generalize domain (#33511) Generalize some lemmas to maps between any 2 normed spaces. Also fix their docstrings.

Estimated changes

Modified Mathlib/Analysis/Complex/Schwarz.lean

modified theorem Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div'

deleted theorem Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div

added theorem Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div

added theorem Complex.dist_le_dist_of_mapsTo_ball

deleted theorem Complex.dist_le_dist_of_mapsTo_ball_self

added theorem Complex.norm_fderiv_le_div_of_mapsTo_ball

added theorem Complex.norm_fderiv_le_one_of_mapsTo_ball

added theorem Complex.norm_le_norm_of_mapsTo_ball

deleted theorem Complex.norm_le_norm_of_mapsTo_ball_self

modified theorem Complex.schwarz_aux