Should "analytic in charts" be `MAnalytic` or `Holomorphic`?

Stream: mathlib4

[Geoffrey Irving]

Once https://github.com/leanprover-community/mathlib4/pull/10853 lands we'll have AnalyticManifold. The next step is to port over the analogue of Smooth, namely the notion that a function between two analytic manifolds is locally or globally analytic in charts.

Currently in https://github.com/girving/ray I call this HolomorphicAt and similar, mostly for the bad reason that MAnalyticAt sounded weirded ("man-alytic").

Should I change the names to MAnalyticAt before upstreaming, or is HolomorphicAt better?

[Yury G. Kudryashov]

The issue with HolomorphicAt is that I only saw this terminology applied to Complex, not other base fields.

[Johan Commelin]

Would Manifold.AnalyticAt work? Should we move docs#AnalyticAt into a namespace?

[Sébastien Gouëzel]

I'd go for MAnalyticAt, to follow the same naming scheme as for smooth functions, even if I agree it's just a little bit awkward. For me, holomorphic is just in the complex setting, you would never say that a real function is holomorphic.

[Geoffrey Irving]

Johan Commelin said:

Would Manifold.AnalyticAt work? Should we move docs#AnalyticAt into a namespace?

I have a lot of files that jump back and forth between the manifold and flat versions a lot, so namespaces would be awkward.