coeff_pow_of_natDegree_le — Mathlib

English

If natDegree(p) ≤ n, then the coefficient of p^m at degree m n equals (coeff p at n)^m.

Русский

Пусть natDegree(p) ≤ n. Тогда коэффициент при p^m на степени m n равен (coeff p на n)^m.

LaTeX

$$$\operatorname{natDegree}(p) \le n \Rightarrow (p^{m}).\coeff(m n) = (\operatorname{coeff} p n)^{m}$$$

Lean4

theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (m * n) = p.coeff n ^ m := by
  induction m with
  | zero => simp
  | succ m hm =>
    rw [pow_succ, pow_succ, ← hm, Nat.succ_mul, coeff_mul_add_eq_of_natDegree_le _ pn]
    refine natDegree_pow_le.trans (le_trans ?_ (le_refl _))
    exact mul_le_mul_of_nonneg_left pn m.zero_le

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