meromorphicNFAt_mul_iff_right — Mathlib

English

If analytic g at x with g(x) ≠ 0, then MeromorphicNFAt (g * f) x ↔ MeromorphicNFAt f x.

Русский

Если аналитично f на x и g(x) ≠ 0, то MeromorphicNFAt (g · f) x эквивалентно MeromorphicNFAt f x.

LaTeX

$$$AnalyticAt\ 𝕜\ g\ x \land g\ x \neq 0 \Rightarrow MeromorphicNFAt\ (g \cdot f)\ x \iff MeromorphicNFAt\ f\ x$$$

Lean4

/-- If `f` is any function and `g` is analytic without zero at `z₀`, then `f` is meromorphic in
normal form at `z₀` iff `g * f` is meromorphic in normal form at `z₀`. -/
theorem meromorphicNFAt_mul_iff_right {f : 𝕜 → 𝕜} (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) :
    MeromorphicNFAt (g * f) x ↔ MeromorphicNFAt f x :=
  meromorphicNFAt_smul_iff_right_of_analyticAt h₁g h₂g

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