Def SemidirectProduct.mulEquivProd

Modification history

2025-01-22 13:15
Mathlib/GroupTheory/SemidirectProduct.lean
feat(GroupTheory/SemidirectProduct): add two lemmas (#20634) …
Added SemidirectProduct.mulEquivProdView on Github →