Def SMulCommClass.toMulActionHom

Modification history

2024-04-05 00:53

Mathlib/GroupTheory/GroupAction/Hom.lean

feat: MulActionHom in the semilinear style (#6057) …

Modified SMulCommClass.toMulActionHom View on Github →

2023-08-10 19:52

Mathlib/Algebra/Hom/GroupAction.lean

chore: banish `Type _` and `Sort _` (#6499) …

Modified SMulCommClass.toMulActionHom View on Github →

2023-06-29 07:18

Mathlib/Algebra/Hom/GroupAction.lean

feat: actions of `DomMulAct` on `A →[N] B` and `A →+[N] B` (#5378) …

Added SMulCommClass.toMulActionHom View on Github →