meromorphicNFAt_mul_iff_left — Mathlib

English

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

Русский

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

LaTeX

$$$AnalyticAt\ 𝕜\ g\ x \land g\ x \neq 0 \Rightarrow MeromorphicNFAt\ (f \cdot g)\ 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 `f * g` is meromorphic in normal form at `z₀`. -/
theorem meromorphicNFAt_mul_iff_left {f : 𝕜 → 𝕜} (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) :
    MeromorphicNFAt (f * g) x ↔ MeromorphicNFAt f x :=
  by
  rw [mul_comm, ← smul_eq_mul]
  exact meromorphicNFAt_smul_iff_right_of_analyticAt h₁g h₂g

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