Commit 2023-06-09 16:21 0c2078a5

View on Github →

feat: port Analysis.Complex.Schwarz (#4910)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Schwarz.lean

added theorem Complex.abs_deriv_le_div_of_mapsTo_ball

added theorem Complex.abs_deriv_le_one_of_mapsTo_ball

added theorem Complex.abs_le_abs_of_mapsTo_ball_self

added theorem Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div'

added theorem Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div

added theorem Complex.dist_le_dist_of_mapsTo_ball_self

added theorem Complex.dist_le_div_mul_dist_of_mapsTo_ball

added theorem Complex.norm_deriv_le_div_of_mapsTo_ball

added theorem Complex.norm_dslope_le_div_of_mapsTo_ball

added theorem Complex.schwarz_aux