eq_X_mul_shift_add_const — Mathlib

English

A form of decomposition: φ equals X times a shifted version plus its constant term.

Русский

Существование разложения: φ = X · mk(...) + C(constantCoeff φ).

LaTeX

$$$\\forall R\\ [\\operatorname{Semiring} R], \\ φ\\in R\\llbracket X\\rrbracket,\\ φ = X \\cdot \\mathrm{mk} (\\lambda p, \\operatorname{coeff}(p+1)\\phi) + C(\\operatorname{constantCoeff}(\\phi))$$$

Lean4

/-- Split off the constant coefficient. -/
theorem eq_X_mul_shift_add_const (φ : R⟦X⟧) : φ = (X * mk fun p => coeff (p + 1) φ) + C (constantCoeff φ) :=
  by
  ext (_ | n)
  · simp only [coeff_zero_eq_constantCoeff, map_add, map_mul, constantCoeff_X, zero_mul, coeff_zero_C, zero_add]
  · simp only [coeff_succ_X_mul, coeff_mk, LinearMap.map_add, coeff_C, n.succ_ne_zero, if_false, add_zero]

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