basic): The centralizer of a characteristic subgroup is characteristic (#13230)

Commit

3 years ago

feat(group_theory/subgroup/basic): The centralizer of a characteristic subgroup is characteristic (#13230) This PR proves that the centralizer of a characteristic subgroup is characteristic.

Author

tb65536

Parents

95ebbadb

mathlib e85dc17a - feat(group_theory/subgroup/basic): The centralizer of a characteristic subgroup is characteristic (#13230)

mathlib
e85dc17a - feat(group_theory/subgroup/basic): The centralizer of a characteristic subgroup is characteristic (#13230)