eraseLead_add_C_mul_X_pow — Mathlib

English

Adding back the constant term, via the leading coefficient, and the monomial recovers the original polynomial.

Русский

Возврат ведущего коэффициента через константный множитель и мононом восстанавливает исходный многочлен.

LaTeX

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

Lean4

@[simp]
theorem eraseLead_add_C_mul_X_pow (f : R[X]) : f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f := by
  rw [C_mul_X_pow_eq_monomial, eraseLead_add_monomial_natDegree_leadingCoeff]

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