gal_X_pow_isSolvable

Mathlib.FieldTheory.AbelRuffini

URI: https://scilib.ai/kg/mathlib#gal_X_pow_isSolvable

English

For any n, the Galois group of X^n over F is solvable.

Русский

Для любого n галуа-группа многочлена X^n над F разрешима.

LaTeX

$$$\\forall n \\in \\mathbb{N}, IsSolvable (X^n : F[X]).Gal$$$

Lean4

theorem gal_X_pow_isSolvable (n : ℕ) : IsSolvable (X ^ n : F[X]).Gal := by infer_instance

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

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

Разделы

Аффилиация

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