Commit 2023-06-09 13:12 03854c5d

View on Github →

feat: port Analysis.Complex.Liouville (#4894)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Complex/Liouville.lean

added theorem Complex.deriv_eq_smul_circleIntegral

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