mathlib3
b72300f3 - feat(group_theory/sylow): all max groups normal imply sylow normal (#11841)

Commit

3 years ago

feat(group_theory/sylow): all max groups normal imply sylow normal (#11841) Co-authored-by: Johan Commelin <johan@commelin.net>

Author

nomeata

Parents