mathlib3
2b257230 - feat(group_theory/sylow): add characteristic_of_normal (#11636)

Commit

4 years ago

feat(group_theory/sylow): add characteristic_of_normal (#11636) A normal sylow subgroup is characteristic. Co-authored-by: Johan Commelin <johan@commelin.net>

Author

nomeata

Parents

1a72f887

mathlib3 2b257230 - feat(group_theory/sylow): add characteristic_of_normal (#11636)

mathlib3
2b257230 - feat(group_theory/sylow): add characteristic_of_normal (#11636)