gal_isSolvable_of_splits — Mathlib

English

If p splits over the SplittingField of q and q.Gal is solvable, then p.Gal is solvable.

Русский

Если p распадается над SplittingField q и q.Gal разрешима, тогда p.Gal разрешим.

LaTeX

$$$\\text{p.Splits (algebraMap F q.SplittingField)} \\Rightarrow IsSolvable q.Gal \\Rightarrow IsSolvable p.Gal$$$

Lean4

theorem gal_isSolvable_of_splits {p q : F[X]} (_ : Fact (p.Splits (algebraMap F q.SplittingField)))
    (hq : IsSolvable q.Gal) : IsSolvable p.Gal :=
  haveI : IsSolvable (q.SplittingField ≃ₐ[F] q.SplittingField) := hq
  solvable_of_surjective (AlgEquiv.restrictNormalHom_surjective q.SplittingField)

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