meromorphicNFOn_smul_iff_right_of_analyticOnNhd

English

MeromorphicNFOn (g * f) U ↔ MeromorphicNFOn f U when g is analytic with g ≠ 0 on U.

Русский

MeromorphicNFOn (g * f) U ⇔ MeromorphicNFOn f U при аналитичности g и g ≠ 0 на U.

LaTeX

$$$MeromorphicNFOn (g * f) U \iff MeromorphicNFOn f U$$$

Lean4

/-- If `f` is any function and `g` is analytic without zero on `U`, then `f` is
meromorphic in normal form on `U` iff `g • f` is meromorphic in normal form on
`U`.
-/
theorem meromorphicNFOn_smul_iff_right_of_analyticOnNhd {g : 𝕜 → 𝕜} (h₁g : AnalyticOnNhd 𝕜 g U)
    (h₂g : ∀ u ∈ U, g u ≠ 0) : MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U :=
  by
  constructor <;> intro h z hz
  · rw [← meromorphicNFAt_smul_iff_right_of_analyticAt (h₁g z hz) (h₂g z hz)]
    exact h hz
  · apply (h hz).smul_analytic (h₁g z hz)
    exact h₂g z hz

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