Commit 2025-05-14 13:17 179655ba

refactor: use a junk value for the analytic order of a non-analytic function (#22974) Currently, the order of an analytic function is called AnalyticAt.order and has a single explicit argument hf : AnalyticAt 𝕜 f z₀. This means that working with analytic functions results in contexts full of hf.order or, worse, ⋯.order. This PR makes the f and z₀ arguments explicit, and drops the hf one by introducing a junk value of 0 for non-analytic functions. The resulting function is called analyticOrderAt and I am also adding a Nat-valued version analyticOrderNatAt since (analyticOrderAt f z₀).toNat was appearing in quite a few lemmas.