English
The trailing coefficient of a finite product equals the finite product of trailing coefficients.
Русский
Хвостовой коэффициент конечного произведения равен произведению хвостовых коэффициентов.
LaTeX
$$$$ \mathrm{meromorphicTrailingCoeffAt}(\prod_{n\in s} f(n), x) = \prod_{n\in s} \mathrm{meromorphicTrailingCoeffAt}(f(n), x). $$$$
Lean4
/-- The trailing coefficient of a product is the product of the trailing coefficients.
-/
theorem meromorphicTrailingCoeffAt_prod {ι : Type*} {s : Finset ι} {f : ι → 𝕜 → 𝕜} {x : 𝕜}
(h : ∀ σ, MeromorphicAt (f σ) x) :
meromorphicTrailingCoeffAt (∏ n ∈ s, f n) x = ∏ n ∈ s, meromorphicTrailingCoeffAt (f n) x := by
classical
induction s using Finset.induction with
| empty => apply meromorphicTrailingCoeffAt_const
| insert σ s₁ hσ hind =>
rw [Finset.prod_insert hσ, Finset.prod_insert hσ, (h σ).meromorphicTrailingCoeffAt_mul (MeromorphicAt.prod h), hind]
