X_order_mul_powerSeriesPart — Mathlib

English

If n equals the order of f, then X^n multiplied by f.powerSeriesPart equals f.

Русский

Если n равняется порядку f, то X^n, умноженное на f.powerSeriesPart, даёт f.

LaTeX

$$$\big(\mathrm{PowerSeries.X}^n\big) \cdot f.powerSeriesPart = f \quad\text{при } n = \mathrm{order}(f)$$$

Lean4

theorem X_order_mul_powerSeriesPart {n : ℕ} {f : R⸨X⸩} (hn : n = f.order) :
    (PowerSeries.X ^ n * f.powerSeriesPart : R⟦X⟧) = f := by
  simp only [map_mul, map_pow, ofPowerSeries_X, single_pow, nsmul_eq_mul, mul_one, one_pow, hn,
    single_order_mul_powerSeriesPart]

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