gal_mul_isSolvable — Mathlib

English

If p and q have solvable Galois groups, then the Galois group of p q is solvable.

Русский

Если галуа-группы многочленов p и q разрешимы, то галуа-группа произведения p q разрешима.

LaTeX

$$$IsSolvable p.Gal \\to IsSolvable q.Gal \\to IsSolvable (p q).Gal$$$

Lean4

theorem gal_mul_isSolvable {p q : F[X]} (_ : IsSolvable p.Gal) (_ : IsSolvable q.Gal) : IsSolvable (p * q).Gal :=
  solvable_of_solvable_injective (Gal.restrictProd_injective p q)

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