leadingCoeff_mul_C_of_isUnit — Mathlib

English

If a is a unit in R and p is a polynomial over R, the leading coefficient of p times C a is the leading coefficient of p times a.

Русский

Пусть a является единичным элементом в R и p — многочлен над R. Старшая коэффициента произведения p · C a равна старшей коэффициенте p, умноженной на a.

LaTeX

$$$ \operatorname{leadingCoeff}(p \cdot C a) = \operatorname{leadingCoeff}(p) \cdot a \quad\text{whenever } \mathrm{IsUnit}(a).$$$

Lean4

theorem leadingCoeff_mul_C_of_isUnit (ha : IsUnit a) (p : R[X]) : (p * C a).leadingCoeff = p.leadingCoeff * a := by
  rwa [leadingCoeff, coeff_mul_C, natDegree_mul_C_of_isUnit, leadingCoeff]

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