Def smulOneHom

Modification history

2023-12-16 07:33

Mathlib/GroupTheory/GroupAction/Defs.lean

feat(Algebra/Module/Basic): add RingHom.smulOneHom (#9064) …

Deleted smulOneHom View on Github →

2022-12-06 09:09

Mathlib/GroupTheory/GroupAction/Defs.lean

feat: port group_theory.group_action.defs (#854) …

Added smulOneHom View on Github →