English
Every power series φ can be written as the sum of X times a shifted version of φ plus its constant term.
Русский
Каждый ряд φ can быть представлен как сумма X умноженного на сдвинутую версию φ и его постоянного коэффициента.
LaTeX
$$$\\forall R\\ [\\operatorname{Semiring} R], \\ φ\\in R\\llbracket X\\rrbracket,\\ φ = (\\mathrm{mk} (\\lambda p, \\operatorname{coeff}(p+1)\\phi))\\cdot X + C(\\operatorname{constantCoeff}(\\phi))$$$
Lean4
/-- Split off the constant coefficient. -/
theorem eq_shift_mul_X_add_const (φ : R⟦X⟧) : φ = (mk fun p => coeff (p + 1) φ) * X + C (constantCoeff φ) :=
by
ext (_ | n)
· simp only [coeff_zero_eq_constantCoeff, map_add, map_mul, constantCoeff_X, mul_zero, coeff_zero_C, zero_add]
· simp only [coeff_succ_mul_X, coeff_mk, LinearMap.map_add, coeff_C, n.succ_ne_zero, if_false, add_zero]
