Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-27 21:28 b5faa34b

View on Github →

feat(analysis/complex/liouville): prove Liouville's theorem (#12095)

Estimated changes

Created src/analysis/complex/liouville.lean

added theorem complex.deriv_eq_smul_circle_integral

added theorem complex.liouville_theorem_aux

added theorem complex.norm_deriv_le_aux

added theorem complex.norm_deriv_le_of_forall_mem_sphere_norm_le

added theorem differentiable.apply_eq_apply_of_bounded

added theorem differentiable.exists_const_forall_eq_of_bounded

added theorem differentiable.exists_eq_const_of_bounded