gal_zero_isSolvable — Mathlib

English

If every polynomial in a multiset s has solvable Galois group, then the Galois group of the product polynomial s.prod is solvable.

Русский

Если для каждого p в мультимножества s галуа-группа выполнима, то галуа-группа произведения p в s.prod выполнима.

LaTeX

$$$\\forall p \\in s, IsSolvable(p.Gal) \\Rightarrow IsSolvable(s.prod.Gal)$$$

Lean4

theorem gal_zero_isSolvable : IsSolvable (0 : F[X]).Gal := by infer_instance

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