Def SMulHomClass.toMulActionHom

Modification history

2024-04-05 00:53

Mathlib/GroupTheory/GroupAction/Hom.lean

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

Deleted SMulHomClass.toMulActionHom View on Github →

2024-02-05 18:00

Mathlib/GroupTheory/GroupAction/Hom.lean

refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …

Modified SMulHomClass.toMulActionHom View on Github →

2023-01-16 10:37

Mathlib/Algebra/Hom/GroupAction.lean

feat: port Algebra.Hom.GroupAction (#1424)

Added SMulHomClass.toMulActionHom View on Github →