meromorphicNFOn_mul_iff_right_of_analyticOnNhd

English

MeromorphicNFOn (f * g) U ↔ MeromorphicNFOn f U under the same hypotheses as above with left multiplication.

Русский

MeromorphicNFOn (f * g) U ⇔ MeromorphicNFOn f U при тех же предположениях слева.

LaTeX

$$$MeromorphicNFOn (f * g) 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 `g * f` is meromorphic in normal form on
`U`.
-/
theorem meromorphicNFOn_mul_iff_right_of_analyticOnNhd {f g : 𝕜 → 𝕜} (h₁g : AnalyticOnNhd 𝕜 g U)
    (h₂g : ∀ u ∈ U, g u ≠ 0) : MeromorphicNFOn (g * f) U ↔ MeromorphicNFOn f U :=
  by
  rw [← smul_eq_mul]
  exact meromorphicNFOn_smul_iff_right_of_analyticOnNhd h₁g h₂g

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