C_mul_X_pow_eq_self — Mathlib

English

If the support of p has at most one element, then C(p.leadingCoeff) · X^{natDegree(p)} equals p.

Русский

Если поддержка p содержит не более одного элемента, то C(p.leadingCoeff) · X^{natDegree(p)} = p.

LaTeX

$$$\\#p.\\operatorname{support} \\le 1 \\Rightarrow C(p.leadingCoeff) \\cdot X^{p.natDegree} = p$$$

Lean4

theorem C_mul_X_pow_eq_self (h : #p.support ≤ 1) : C p.leadingCoeff * X ^ p.natDegree = p := by
  rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]

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