English
If f1 and f2 are meromorphic on U and f1 agrees with f2 on codiscreteWithin U, then their divisors on U are equal (assuming U open).
Русский
Если f1 и f2 мероморфны на U и совпадают на codiscreteWithin U, то делители на U равны (при условии открытости U).
LaTeX
$$$\text{MeromorphicOn}(f_1, U) \to (f_1 =\!\!\!\!_{\text{codiscreteWithin }U} f_2) \to \text{IsOpen}(U) \Rightarrow \text{divisor}(f_1, U) = \text{divisor}(f_2, U)$$$
Lean4
/-- Simplifier lemma: on `U`, the divisor of a function `f` that is meromorphic on `U` evaluates to
`order.untop₀`.
-/
@[simp]
theorem divisor_apply {f : 𝕜 → E} (hf : MeromorphicOn f U) (hz : z ∈ U) :
divisor f U z = (meromorphicOrderAt f z).untop₀ := by simp_all [MeromorphicOn.divisor_def]
