Commit 2025-02-07 17:49 2106ab5f

chore(GroupExtension/Basic): add lemmas about extensions by (non-abelian) groups (#20998) As the second part of #19582, this PR mostly contains the changes to the Basic file. It mainly:

• redefines GroupExtension.Equiv with MulEquiv rather than MonoidHom;
• adds lemmas that do not require a commutative group, as a preparation for the main PR;
• defines GroupExtension.Splitting.semidirectProductMulEquiv, an isomorphism between the group associated to a split extension and a semidirect product; and
• defines GroupExtension.ConjClasses, the conjugacy classes of splittings. It also contains some definitions and lemmas unused in the main PR, such as:
• GroupExtension.quotientRangeInlEquivRight, provided as a shorthand for end-users; and
• GroupExtension.Section.section_inv_mul_mem_range, provided as a symmetric counterpart of a required lemma. They may be dropped if this PR would introduce a too large diff. Moves:
• GroupExtension.Equiv.mk -> GroupExtension.Equiv.ofMonoidHom