aroots_pow

Mathlib.Algebra.Polynomial.Roots

URI: https://scilib.ai/kg/mathlib#Polynomial.aroots_pow

← MathLib Explorer

English

The roots of p^n are n copies of the roots of p: (p^n) ar roots = n · (p.aroots).

Русский

Корни p^n — это n копий корней p: (p^n) arroots = n · (p.aroots).

LaTeX

$$$$ (p^n)\aroots_S = n \cdot (p\aroots_S) $$$$

Lean4

@[simp]
theorem aroots_pow [CommRing S] [IsDomain S] [Algebra T S] (p : T[X]) (n : ℕ) : (p ^ n).aroots S = n • p.aroots S := by
  rw [aroots_def, Polynomial.map_pow, roots_pow]

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru