sub_const_eq_X_mul_shift — Mathlib

English

For φ, φ − C(const φ) equals X times mk with coefficients coeff (p+1) φ.

Русский

Для φ разность φ и C(const φ) равна X умноженному на mk со сдвигом коэффициентов: coeff (p+1) φ.

LaTeX

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

Lean4

theorem sub_const_eq_X_mul_shift (φ : R⟦X⟧) : φ - C (constantCoeff φ) = X * mk fun p ↦ coeff (p + 1) φ :=
  sub_eq_iff_eq_add.mpr (eq_X_mul_shift_add_const φ)

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