meromorphicNFOn_mul_iff_left_of_analyticOnNhd

English

If analytic g on a punctured neighborhood with nonvanishing values, then MeromorphicNFOn (g • f) U ↔ MeromorphicNFOn f U.

Русский

Если g аналитична в окрестности без точки x и g не нуль на U, то MeromorphicNFOn (g • f) U ⇔ MeromorphicNFOn f U.

LaTeX

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

Lean4

/-- If `f` is any function and `g` is analytic without zero in `U`, then `f` is
meromorphic in normal form on `U` iff `f * g` is meromorphic in normal form on
`U`.
-/
theorem meromorphicNFOn_mul_iff_left_of_analyticOnNhd {f g : 𝕜 → 𝕜} (h₁g : AnalyticOnNhd 𝕜 g U)
    (h₂g : ∀ u ∈ U, g u ≠ 0) : MeromorphicNFOn (f * g) U ↔ MeromorphicNFOn f U :=
  by
  rw [mul_comm, ← smul_eq_mul]
  exact meromorphicNFOn_mul_iff_right_of_analyticOnNhd h₁g h₂g

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