Local quotient cancellation at a zero, counting multiplicity.
If f and g are analytic at a and have the same (finite) vanishing order at a, then the
quotient f/g has a removable singularity at a. We package this by constructing an explicit
piecewise definition that is analytic at a.
This is the pointwise ingredient needed to upgrade the “simple zeros” quotient arguments to the general multiplicity regime.
theorem
Hadamard.OrderOne.exists_analyticAt_update_div_of_analyticOrderNatAt_eq
{f g : ℂ → ℂ}
{a : ℂ}
(hf : AnalyticAt ℂ f a)
(hg : AnalyticAt ℂ g a)
(hf' : analyticOrderAt f a ≠ ⊤)
(hg' : analyticOrderAt g a ≠ ⊤)
(hord : analyticOrderNatAt f a = analyticOrderNatAt g a)
: