aroots_C

Mathlib.Algebra.Polynomial.Roots

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

English

A constant polynomial C(a) has no roots in a domain; its root multiset is empty.

Русский

Константный многочлен C(a) не имеет корней в области; множество корней пусто.

LaTeX

$$$$ (C(a))\aroots_S = 0 $$$$

Lean4

@[simp]
theorem aroots_C [CommRing S] [IsDomain S] [Algebra T S] (a : T) : (C a).aroots S = 0 := by
  rw [aroots_def, map_C, roots_C]

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

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

Разделы

Аффилиация

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