Def DistribMulAction.prodEquiv

Modification history

2023-11-30 16:55
Mathlib/GroupTheory/GroupAction/Prod.lean
feat: MulAction by product monoid (#8634) …
Added DistribMulAction.prodEquivView on Github →