mathlib

6a966c80 - chore(geometry/manifold/complex): extract some theory of locally constant functions (#16019)

chore(geometry/manifold/complex): extract some theory of locally constant functions (#16019) After #16015, I realised that we might as well deduce the rest of the lemmas in the file from the `is_locally_constant` lemma by appealing to general theory about locally constant functions. I have added three such lemmas to the general theory of locally constant functions: * `is_locally_constant.apply_eq_of_preconnected_space` * `is_locally_constant.eq_const` * `is_locally_constant.exists_eq_const` All are direct copies of the lemmas for the bundled version (`locally_constant`). Then I reworked the holomorphic function theory to pass through these, which cuts a few lines from the file.