Def MonoidHom.smulOneHom

Modification history

2024-10-24 19:49

Mathlib/Algebra/Group/Action/Defs.lean

chore(Algebra/Group/Action): reduce theory included with `Group.Action.Defs` (#18187) …

Modified MonoidHom.smulOneHom View on Github →

2024-05-24 03:47

Mathlib/Algebra/Group/Action/Defs.lean

chore: Move `MulAction` to under `Algebra` (#13140) …

Modified MonoidHom.smulOneHom View on Github →

2023-12-16 07:33

Mathlib/GroupTheory/GroupAction/Defs.lean

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

Added MonoidHom.smulOneHom View on Github →