self_sub_C_mul_X_pow — Mathlib

English

Subtracting the leading coefficient times X^natDegree from f equals eraseLead f.

Русский

Вычитание ведущего коэффициента, умноженного на X^natDegree, из f равно eraseLead(f).

LaTeX

$$f - C(f.leadingCoeff) * X ^ f.natDegree = f.eraseLead$$

Lean4

@[simp]
theorem self_sub_C_mul_X_pow {R : Type*} [Ring R] (f : R[X]) : f - C f.leadingCoeff * X ^ f.natDegree = f.eraseLead :=
  by rw [C_mul_X_pow_eq_monomial, self_sub_monomial_natDegree_leadingCoeff]

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