coeff_pow_nsmul_degree — Mathlib

English

For a polynomial f and natural n, the coefficient of the monomial at degree n · deg f in f^n equals the leading coefficient of f raised to n: (f^n)_{n·deg f} = (lc_m f)^n.

Русский

Для многочлена f и натурального n коэффициент при мономе степени n · deg f в f^n равен (lc_m f)^n.

LaTeX

$$$$ (f^n)_{n\cdot \deg_m f} = (\operatorname{leadingCoeff}_m f)^n. $$$$

Lean4

theorem coeff_pow_nsmul_degree (f : MvPolynomial σ R) (n : ℕ) : (f ^ n).coeff (n • m.degree f) = m.leadingCoeff f ^ n :=
  by
  induction n with
  | zero => simp
  | succ n hrec =>
    simp only [add_smul, one_smul, pow_add, pow_one]
    rw [m.coeff_mul_of_add_of_degree_le (m.degree_pow_le _) le_rfl, hrec, leadingCoeff]

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