Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-17 14:43 50bdb297

View on Github →

feat(analysis/complex/cauchy_integral): review docs, add versions without off_countable (#11417)

Estimated changes

Modified src/analysis/complex/cauchy_integral.lean

added theorem complex.circle_integral_sub_inv_smul_of_continuous_on_of_differentiable_on

added theorem complex.circle_integral_sub_inv_smul_of_differentiable_on

added theorem complex.has_fpower_series_on_ball_of_continuous_on_of_differentiable_on

added theorem complex.integral_boundary_rect_eq_zero_of_continuous_on_of_differentiable_on

added theorem complex.integral_boundary_rect_eq_zero_of_differentiable_on

added theorem complex.integral_boundary_rect_of_continuous_on_of_has_fderiv_at_real

added theorem complex.integral_boundary_rect_of_differentiable_on_real

added theorem complex.integral_boundary_rect_of_has_fderiv_at_real_off_countable

deleted theorem complex.integral_boundary_rect_of_has_fderiv_within_at_real_off_countable

Modified src/analysis/complex/re_im_topology.lean

added theorem is_closed.re_prod_im

added theorem is_open.re_prod_im