English
If f is meromorphic in normal form at x and g is analytic without zero at x, then g • f is meromorphic in normal form at x.
Русский
Если f мероморфна в нормальной форме в x и g аналитична и не обращается в нуль в x, то g • f тоже мероморфна в нормальной форме в x.
LaTeX
$$$MeromorphicNFAt\ f\ x \land AnalyticAt\ 𝕜\ g\ x \land g\ x \neq 0 \Rightarrow MeromorphicNFAt\ (g \cdot f)\ x$$$
Lean4
/-- Helper lemma for `meromorphicNFAt_iff_meromorphicNFAt_of_smul_analytic`: if
`f` is meromorphic in normal form at `x` and `g` is analytic without zero at
`x`, then `g • f` is meromorphic in normal form at `x`. -/
theorem smul_analytic (hf : MeromorphicNFAt f x) (h₁g : AnalyticAt 𝕜 g x) (h₂g : g x ≠ 0) : MeromorphicNFAt (g • f) x :=
by
rcases hf with h₁f | ⟨n, g_f, h₁g_f, h₂g_f, h₃g_f⟩
· left
filter_upwards [h₁f]
simp_all
· right
use n, g • g_f, h₁g.smul h₁g_f
constructor
· simp [smul_ne_zero h₂g h₂g_f]
· filter_upwards [h₃g_f]
intro y hy
simp only [Pi.smul_apply', hy, Pi.pow_apply]
rw [smul_comm]
