leadingCoeff_smul_of_smul_regular

English

Let R be a semiring and k act regularly on R. Then for every polynomial p ∈ R[X], the leading coefficient commutes with scaling: lc(k · p) = k · lc(p).

Русский

Пусть R - полускольное кольцо и k действует на R регулярно. Тогда для любого многочлена p ∈ R[X] ведущий коэффициент сохраняется под умножением: lc(k · p) = k · lc(p).

LaTeX

$$$\\operatorname{leadingCoeff}(k \cdot p) = k \cdot \operatorname{leadingCoeff}(p).$$$

Lean4

theorem leadingCoeff_smul_of_smul_regular {S : Type*} [SMulZeroClass S R] {k : S} (p : R[X]) (h : IsSMulRegular R k) :
    (k • p).leadingCoeff = k • p.leadingCoeff := by
  rw [Polynomial.leadingCoeff, Polynomial.leadingCoeff, coeff_smul, natDegree_smul_of_smul_regular p h]

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