mathlib3
2234ee3c - feat(group_theory/sylow): add characteristic_of_normal

Commit

4 years ago

feat(group_theory/sylow): add characteristic_of_normal A normal sylow is characteristic.

Author

nomeata

Parents