mathlib

1df93013 - feat(group_theory/semidirect_product): introduce semidirect_products of groups (#3028)