Commit 2025-02-05 04:27 460a8b09

feat/doc: split files, add documentation (#21421) Move the material on orders of analytic functions out of the file Mathlib/Analysis/Analytic/IsolatedZeros.lean. Create a directory Mathlib/Analysis/Meromorphic. Move the file Mathlib/Analysis/Analytic/Meromorphic.lean to Mathlib/Analysis/Meromorphic/Basic.lean. Move the material on orders of meromorphic functions to the file Mathlib/Analysis/Meromorphic/Order.lean. Add documentation. This PR does not add new theorems or change existing ones. As discussed with @TwoFX (and others) during the Lean Meeting at Freiburg, I would like to move material on orders of analytic/meromorphic functions to independent files. Reasons:

• The material on order in Mathlib/Analysis/Analytic/IsolatedZeros.lean was never referenced from anywhere else in this file. This is now seen by the fact that Mathlib/Analysis/Analytic/IsolatedZeros.lean does not reference the new file Mathlib/Analysis/Analytic/Order.lean. Similarly in the meromorphic setting.
• The material on orders is bound to grow quite a bit, as I plan to add the missing material on the behavior of orders under addition and composition, both in the analytic and meromorphic settings. I will also need to say more about the topology of the level sets.
• I intend to add more material on meromorphic functions, including a discussion of (and API for) continuous extension, and extraction of zeros/poles. The amount of material justifies that meromorphic functions get their own directory.