Commit 2024-02-15 16:15 8257db38

View on Github →

chore(FieldTheory/PolynomialGaloisGroup): move lemmas, reduce imports (#9886) #dependencies: Mathlib.FieldTheory.PolynomialGaloisGroup: 1826->1323 Mathlib.Analysis.Complex.Polynomial: 1811->1826 This needed one small change to a moved proof because conj is not allowed as an identifier when the ComplexConjugate locale is open.

Estimated changes

Modified Archive/Wiedijk100Theorems/AbelRuffini.lean

Modified Mathlib/Analysis/Complex/Polynomial.lean

added theorem Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv

added theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree'

added theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree

added theorem Polynomial.Gal.splits_ℚ_ℂ

Modified Mathlib/FieldTheory/PolynomialGaloisGroup.lean

deleted theorem Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv

deleted theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree'

deleted theorem Polynomial.Gal.galActionHom_bijective_of_prime_degree

deleted theorem Polynomial.Gal.splits_ℚ_ℂ