Commit 2023-06-27 14:29 87f75bd0

View on Github →

feat: port Geometry.Manifold.Complex (#5498)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Manifold/Complex.lean

added theorem Complex.norm_eventually_eq_of_mdifferentiableAt_of_isLocalMax

added theorem MDifferentiable.apply_eq_of_compactSpace

added theorem MDifferentiable.exists_eq_const_of_compactSpace

added theorem MDifferentiableOn.apply_eq_of_isPreconnected_isCompact_isOpen

added theorem MDifferentiableOn.eqOn_of_isPreconnected_of_isMaxOn_norm

added theorem MDifferentiableOn.norm_eqOn_of_isPreconnected_of_isMaxOn