Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 08:31 0f3bfda7

View on Github →

feat(analysis/complex/schwarz): some versions of the Schwarz lemma (#12633)

Estimated changes

Modified src/analysis/calculus/dslope.lean

added theorem continuous_linear_map.dslope_comp

Modified src/analysis/complex/removable_singularity.lean

Created src/analysis/complex/schwarz.lean

added theorem complex.abs_deriv_le_div_of_maps_to_ball

added theorem complex.abs_deriv_le_one_of_maps_to_ball

added theorem complex.abs_le_abs_of_maps_to_ball_self

added theorem complex.dist_le_dist_of_maps_to_ball_self

added theorem complex.dist_le_div_mul_dist_of_maps_to_ball

added theorem complex.norm_deriv_le_div_of_maps_to_ball

added theorem complex.norm_dslope_le_div_of_maps_to_ball

added theorem complex.schwarz_aux

Modified src/linear_algebra/affine_space/slope.lean

added theorem affine_map.slope_comp

added theorem linear_map.slope_comp