Theorem GroupExtension.Splitting.rightHom_comp_splitting

Modification history

2025-01-17 06:22
Mathlib/GroupTheory/GroupExtension/Defs.lean
chore(GroupExtension/Defs): define `Section` and redefine `Splitting` (#20802) …
Added GroupExtension.Splitting.rightHom_comp_splittingView on Github →