theorem GaloisTheory.card_aut_le_finrank (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] : Nat.card Gal(E/F) ≤ Module.finrank F E

theorem GaloisTheory.isGalois_iff_card_aut_eq_finrank (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] : IsGalois F E ↔ Nat.card Gal(E/F) = Module.finrank F E

theorem GaloisTheory.galois_group_size (F : Type u_3) (E : Type u_4) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] [Algebra.IsSeparable F E] : Nat.card Gal(E/F) ≤ Module.finrank F E ∧ (IsGalois F E ↔ Nat.card Gal(E/F) = Module.finrank F E)

noncomputable def GaloisTheory.fundamentalTheoremSymmetricPolynomials (σ : Type u_3) (R : Type u_4) {n : ℕ} [Fintype σ] [CommRing R] (hn : Fintype.card σ = n) : MvPolynomial (Fin n) R ≃ₐ[R] ↥(MvPolynomial.symmetricSubalgebra σ R)

theorem GaloisTheory.symmetric_polynomial_in_esymm {F : Type u_3} [Field F] {P : Polynomial F} (hP : P.Monic) (hsplit : P.Splits) (n : ℕ) (hn : P.natDegree = n) (f : MvPolynomial (Fin n) F) (hf : f.IsSymmetric) (α : Fin n → F) (hα : P = ∏ i : Fin n, (Polynomial.X - Polynomial.C (α i))) : ∃ (q : MvPolynomial (Fin n) F), (MvPolynomial.eval α) f = (MvPolynomial.eval fun (i : Fin n) => (-1) ^ (↑i + 1) * P.coeff (n - (↑i + 1))) q

theorem GaloisTheory.all_minpoly_split_in_splitting_field {F : Type u_3} [Field F] (p : Polynomial F) (α : p.SplittingField) : (Polynomial.map (algebraMap F p.SplittingField) (minpoly F α)).Splits

@[reducible, inline]

abbrev GaloisTheory.IsSolvableGroup (G : Type u_3) [Group G] : Prop

theorem GaloisTheory.s5_not_solvable_and_a5_simple : ¬IsSolvable (Equiv.Perm (Fin 5)) ∧ IsSimpleGroup ↥(alternatingGroup (Fin 5))

theorem GaloisTheory.symmetric_group_not_solvable {n : ℕ} (hn : 5 ≤ n) : ¬IsSolvable (Equiv.Perm (Fin n))

theorem GaloisTheory.not_solvableByRad_of_gal_iso_S5 {F : Type u_3} {E : Type u_4} [Field F] [Field E] [Algebra F E] {p : Polynomial F} (hp : Irreducible p) (hiso : p.Gal ≃* Equiv.Perm (Fin 5)) {x : E} (hpx : (Polynomial.aeval x) p = 0) : x ∉ solvableByRad F E