mathlib3

a9f99604 - feat(geometry/manifold/complex): holomorphic functions are locally constant (#16015)

feat(geometry/manifold/complex): holomorphic functions are locally constant (#16015) Prove that a holomorphic function on a compact complex manifold is locally constant. This is nearly a trivial consequence of #15667 and #15965; the only new input is that a charted space modelled on a locally connected space is locally connected.