mathlib
8c7e8a4d - feat(group_theory/commutator): The commutator subgroup is characteristic (#13255)

Commit

3 years ago

feat(group_theory/commutator): The commutator subgroup is characteristic (#13255) This PR adds instances stating that the commutator subgroup is characteristic.

Author

tb65536

Parents

d23fd6f7

mathlib 8c7e8a4d - feat(group_theory/commutator): The commutator subgroup is characteristic (#13255)

mathlib
8c7e8a4d - feat(group_theory/commutator): The commutator subgroup is characteristic (#13255)