sub_const_eq_shift_mul_X — Mathlib

English

For φ, subtracting its constant term is the same as X times a shifted series: φ − C(const φ) = (mk p ↦ coeff (p + 1) φ) · X.

Русский

Из степенного ряда вычитание константного члена равно X умноженному на степенной ряд со сдвигом коэффициентов: φ − C(const φ) = X · mk (p ↦ coeff (p + 1) φ).

LaTeX

$$$ φ - C(\text{constantCoeff } φ) = X \cdot \Big( mk( \; p \mapsto \mathrm{coeff}(p+1) φ \; ) \Big) $$$

Lean4

/-- Two ways of removing the constant coefficient of a power series are the same. -/
theorem sub_const_eq_shift_mul_X (φ : R⟦X⟧) : φ - C (constantCoeff φ) = (mk fun p ↦ coeff (p + 1) φ) * X :=
  sub_eq_iff_eq_add.mpr (eq_shift_mul_X_add_const φ)

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