P

Mathlib.FieldTheory.AbelRuffini

URI: https://scilib.ai/kg/mathlib#solvableByRad.P

English

For α in solvableByRad F E, P α is equivalent to IsSolvable(minpoly F α).Gal.

Русский

Для элемента α из solvableByRad F E, P α эквивалентно IsSolvable(minpoly F α).Gal.

LaTeX

$$$$P(\alpha) \iff IsSolvable\big(\minpoly F \alpha\big).Gal$$$$

Lean4

/-- The statement to be proved inductively -/
def P (α : solvableByRad F E) : Prop :=
  IsSolvable (minpoly F α).Gal

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

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

Разделы

Аффилиация

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