negPart_divisor_add_of_analyticNhdOn_left

English

Adding an analytic function on the left also preserves the pole divisor.

Русский

Добавление аналитической функции слева сохраняет полю делитель.

LaTeX

$$$(\text{divisor}(f_1+ f_2)U)^- = (\text{divisor}(f_2)U)^- $ if f_2 meromorphic on U and f_1 analytic near U$$

Lean4

/-- Adding an analytic function to a meromorphic one does not change the pole divisor. -/
theorem negPart_divisor_add_of_analyticNhdOn_left {f₁ f₂ : 𝕜 → E} (hf₁ : AnalyticOnNhd 𝕜 f₁ U)
    (hf₂ : MeromorphicOn f₂ U) : (divisor (f₁ + f₂) U)⁻ = (divisor f₂ U)⁻ :=
  by
  rw [add_comm]
  exact negPart_divisor_add_of_analyticNhdOn_right hf₂ hf₁

Похожие утверждения