ofPowerSeries_powerSeriesPart — Mathlib

English

The power-series part x.powerSeriesPart is recovered from x by the relation: ofPowerSeries(ℤ, R)(x.powerSeriesPart) = single(-x.order) 1 · x.

Русский

Степенной ряд x.powerSeriesPart восстанавливается из x по формуле: ofPowerSeries(ℤ, R)(x.powerSeriesPart) = single(-order(x)) 1 · x.

LaTeX

$$$\mathrm{ofPowerSeries}(\mathbb{Z}, R)(x.powerSeriesPart) = \big(\text{single}(-\mathrm{order}(x))\, 1\big) \cdot x$$$

Lean4

theorem ofPowerSeries_powerSeriesPart (x : R⸨X⸩) : ofPowerSeries ℤ R x.powerSeriesPart = single (-x.order) 1 * x :=
  by
  refine Eq.trans ?_ (congr rfl x.single_order_mul_powerSeriesPart)
  rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]

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