mathlib
c3ecf005 - feat(group_theory/sylow): direct product of sylow groups if all normal (#11778)

Commit

3 years ago

feat(group_theory/sylow): direct product of sylow groups if all normal (#11778) Co-authored-by: Johan Commelin <johan@commelin.net>

Author

nomeata

Parents