English
Another simplified form of divisor congruence related to codiscreteWithin.
Русский
Ещё одна упрощённая форма конгруэнтности делителя связанная с codiscreteWithin.
LaTeX
$$$\text{MeromorphicOn}(f_1, U) \Rightarrow (f_1 =\!\!\!\!_{\text{codiscreteWithin }U} f_2) \Rightarrow \text{divisor}(f_1, U) = \text{divisor}(f_2, U)$$$
Lean4
/-- If orders are finite, the divisor of the scalar product of two meromorphic functions is the sum of
the divisors.
See `MeromorphicOn.exists_order_ne_top_iff_forall` and
`MeromorphicOn.order_ne_top_of_isPreconnected` for two convenient criteria to guarantee conditions
`h₂f₁` and `h₂f₂`.
-/
theorem divisor_smul {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E} (h₁f₁ : MeromorphicOn f₁ U) (h₁f₂ : MeromorphicOn f₂ U)
(h₂f₁ : ∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) (h₂f₂ : ∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) :
divisor (f₁ • f₂) U = divisor f₁ U + divisor f₂ U := by
ext z
by_cases hz : z ∈ U
· lift meromorphicOrderAt f₁ z to ℤ using (h₂f₁ z hz) with a₁ ha₁
lift meromorphicOrderAt f₂ z to ℤ using (h₂f₂ z hz) with a₂ ha₂
simp [h₁f₁, h₁f₂, h₁f₁.smul h₁f₂, hz, meromorphicOrderAt_smul (h₁f₁ z hz) (h₁f₂ z hz), ← ha₁, ← ha₂,
← WithTop.coe_add]
· simp [hz]
