gal_prod_isSolvable — Mathlib

English

The Galois group of the product of a Multiset of polynomials is solvable if each factor is solvable.

Русский

Галуа-группа произведения множества многочленов решаема, если каждый множитель разрешим.

LaTeX

$$$\\forall s : Multiset F[X], (\\forall p \\in s, IsSolvable p.Gal) \\Rightarrow IsSolvable s.prod.Gal$$$

Lean4

theorem gal_prod_isSolvable {s : Multiset F[X]} (hs : ∀ p ∈ s, IsSolvable (Gal p)) : IsSolvable s.prod.Gal :=
  by
  apply Multiset.induction_on' s
  · exact gal_one_isSolvable
  · intro p t hps _ ht
    rw [Multiset.insert_eq_cons, Multiset.prod_cons]
    exact gal_mul_isSolvable (hs p hps) ht

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