Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-02 04:27 cfc74155

View on Github →

feat(field_theory/polynomial_galois_group): Galois group is S_p (#7352) Proves that a Galois group is isomorphic to S_p, under certain conditions.

Estimated changes

Modified src/data/complex/basic.lean

added theorem complex.eq_conj_iff_im

Modified src/data/complex/module.lean

added def complex.conj_alg_equiv

Modified src/data/fintype/basic.lean

modified theorem set.to_finset_empty

Modified src/data/polynomial/ring_division.lean

added theorem polynomial.root_set_finite

Modified src/field_theory/polynomial_galois_group.lean

added theorem polynomial.gal.gal_action_hom_bijective_of_prime_degree

added theorem polynomial.gal.gal_action_hom_bijective_of_prime_degree_aux

added theorem polynomial.gal.gal_action_hom_restrict

added theorem polynomial.gal.splits_ℚ_ℂ

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.of_injective_apply

added def monoid_hom.of_left_inverse

added theorem monoid_hom.of_left_inverse_apply

added theorem monoid_hom.of_left_inverse_symm_apply