roots_pow — Mathlib

English

For any p ∈ R[X] and n ∈ ℕ, (p^n).roots = n • p.roots.

Русский

Для любого p ∈ R[X] и n ∈ ℕ, корни p^n равны n • p.roots.

LaTeX

$$$ (p^n).roots = n \cdot p.roots $$$

Lean4

@[simp]
theorem roots_pow (p : R[X]) (n : ℕ) : (p ^ n).roots = n • p.roots := by
  induction n with
  | zero => rw [pow_zero, roots_one, zero_smul, empty_eq_zero]
  | succ n ihn =>
    rcases eq_or_ne p 0 with (rfl | hp)
    · rw [zero_pow n.succ_ne_zero, roots_zero, smul_zero]
    · rw [pow_succ, roots_mul (mul_ne_zero (pow_ne_zero _ hp) hp), ihn, add_smul, one_smul]

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