splits_ℚ_ℂ

Mathlib.Analysis.Complex.Polynomial.Basic

URI: https://scilib.ai/kg/mathlib#Polynomial.Gal.splits_ℚ_ℂ

English

For p ∈ ℚ[X], p splits completely over ℂ, i.e., p has all its roots in ℂ.

Русский

Для p ∈ ℚ[X] многочлен раскладывается над ℂ, т.е. все корни лежат в ℂ.

LaTeX

$$$$ \\forall p \\in \\mathbb{Q}[X],\\ p \\text{ splits in } \\mathbb{C}. $$$$

Lean4

theorem splits_ℚ_ℂ {p : ℚ[X]} : Fact (p.Splits (algebraMap ℚ ℂ)) :=
  ⟨IsAlgClosed.splits_codomain p⟩

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

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

Разделы

Аффилиация

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