meromorphicTrailingCoeffAt_mul — Mathlib

English

The trailing coefficient of a product is the product of trailing coefficients.

Русский

Хвостовой коэффициент произведения равен произведению хвостовых коэффициентов.

LaTeX

$$$$ \mathrm{meromorphicTrailingCoeffAt}(f_1 * f_2, x) = \mathrm{meromorphicTrailingCoeffAt}(f_1,x) * \mathrm{meromorphicTrailingCoeffAt}(f_2,x). $$$$

Lean4

/-- The trailing coefficient of a product is the product of the trailing coefficients.
-/
theorem meromorphicTrailingCoeffAt_mul {f₁ f₂ : 𝕜 → 𝕜} (hf₁ : MeromorphicAt f₁ x) (hf₂ : MeromorphicAt f₂ x) :
    meromorphicTrailingCoeffAt (f₁ * f₂) x = (meromorphicTrailingCoeffAt f₁ x) * (meromorphicTrailingCoeffAt f₂ x) :=
  meromorphicTrailingCoeffAt_smul hf₁ hf₂

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