nextCoeff_pow — Mathlib

English

For a monic polynomial p and any n, (p^n).nextCoeff = n · p.nextCoeff.

Русский

Для моноического p и любого n верно (p^n).nextCoeff = n · p.nextCoeff.

LaTeX

$$$Monic(p) \Rightarrow \forall n \in \mathbb{N}, \; (p^n).nextCoeff = n \cdot p.nextCoeff$$$

Lean4

theorem nextCoeff_pow (hp : p.Monic) (n : ℕ) : (p ^ n).nextCoeff = n • p.nextCoeff := by
  induction n with
  | zero => rw [pow_zero, zero_smul, ← map_one (f := C), nextCoeff_C_eq_zero]
  | succ n ih => rw [pow_succ, (hp.pow n).nextCoeff_mul hp, ih, succ_nsmul]

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