leadingCoeff_C_mul_of_isUnit — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem leadingCoeff_C_mul_of_isUnit (ha : IsUnit a) (p : R[X]) : (C a * p).leadingCoeff = a * p.leadingCoeff := by
  rwa [leadingCoeff, coeff_C_mul, natDegree_C_mul_of_isUnit, leadingCoeff]

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