leadingCoeff_pow — Mathlib

English

For any polynomial p and natural n, the leading coefficient of p^n is the nth power of the leading coefficient of p: lc(p^n) = (lc(p))^n.

Русский

Для любого многочлена p и натурального n ведущий коэффициент p^n равен (lc(p))^n.

LaTeX

$$$\operatorname{lc}(p^n)=\bigl(\operatorname{lc}(p)\bigr)^n.$$$

Lean4

@[simp]
theorem leadingCoeff_pow (p : R[X]) (n : ℕ) : leadingCoeff (p ^ n) = leadingCoeff p ^ n :=
  (leadingCoeffHom : R[X] →* R).map_pow p n

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