Commit 2025-01-17 06:22 a1e497db

View on Github →

chore(GroupExtension/Defs): define Section and redefine Splitting (#20802) This PR:

defines structure (Add)?GroupExtension.Section as a right inverse to rightHom
redefines structure (Add)?GroupExtension.Splitting using Section
rewrites the definition of structure (Add)?GroupExtension.Equiv with extends As the first part of #19582, this PR contains only the changes to the Defs file. Moves:
GroupExtension.Splitting.sectionHom -> GroupExtension.Splitting.toMonoidHom
GroupExtension.Splitting.rightHom_comp_sectionHom -> GroupExtension.Splitting.rightInverse_rightHom

Estimated changes

Modified Mathlib/GroupTheory/GroupExtension/Defs.lean

modified structure AddGroupExtension.Equiv

added structure AddGroupExtension.Section

modified structure AddGroupExtension.Splitting

modified structure GroupExtension.Equiv

modified def GroupExtension.IsConj

added theorem GroupExtension.Section.coe_mk

added theorem GroupExtension.Section.rightHom_comp_section

added theorem GroupExtension.Section.rightHom_section

added structure GroupExtension.Section

added theorem GroupExtension.Splitting.coe_mk

added theorem GroupExtension.Splitting.coe_monoidHom_mk

added theorem GroupExtension.Splitting.rightHom_comp_splitting

added theorem GroupExtension.Splitting.rightHom_splitting

modified structure GroupExtension.Splitting