nthRoots_zero_right

Mathlib.Algebra.Polynomial.Roots

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

← MathLib Explorer

English

For any n, the nthRoots of zero equal n copies of zero

Русский

Для любого n корни nthRoots(n, 0) состоят из n копий нуля.

LaTeX

$$$\operatorname{nthRoots}(n, 0) = \operatorname{Multiset.replicate}(n, 0)$$$

Lean4

@[simp]
theorem nthRoots_zero_right {R} [CommRing R] [IsDomain R] (n : ℕ) : nthRoots n (0 : R) = Multiset.replicate n 0 := by
  rw [nthRoots, C.map_zero, sub_zero, roots_pow, roots_X, Multiset.nsmul_singleton]

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

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

Разделы

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

Аффилиация

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