Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 09:30 dec29aa3

View on Github →

feat(group_theory/solvable): S_5 is not solvable (#7453) This is a rather hacky proof that S_5 is not solvable. The proper proof via the simplicity of A_5 will eventually replace this. But until then, this result is needed for abel-ruffini. Most of the work done by Jordan Brown

Estimated changes

Modified src/data/equiv/fintype.lean

deleted def equiv.perm.via_embedding

deleted theorem equiv.perm.via_embedding_apply_image

deleted theorem equiv.perm.via_embedding_apply_mem_range

deleted theorem equiv.perm.via_embedding_apply_not_mem_range

deleted theorem equiv.perm.via_embedding_sign

added def equiv.perm.via_fintype_embedding

added theorem equiv.perm.via_fintype_embedding_apply_image

added theorem equiv.perm.via_fintype_embedding_apply_mem_range

added theorem equiv.perm.via_fintype_embedding_apply_not_mem_range

added theorem equiv.perm.via_fintype_embedding_sign

Modified src/group_theory/perm/basic.lean

added def equiv.perm.extend_domain_hom

added theorem equiv.perm.extend_domain_hom_injective

added theorem equiv.perm.of_subtype_apply_coe

added theorem equiv.perm.via_embedding_apply

added theorem equiv.perm.via_embedding_apply_of_not_mem

added theorem equiv.perm.via_embedding_hom_apply

added theorem equiv.perm.via_embedding_hom_injective

Modified src/group_theory/perm/fin.lean

Modified src/group_theory/solvable.lean

added theorem equiv.perm.fin_5_not_solvable

added theorem equiv.perm.not_solvable

added theorem general_commutator_containment

added theorem not_solvable_of_mem_derived_series