Def MulActionHom.ofEq

Modification history

2024-05-17 19:31

Mathlib/GroupTheory/GroupAction/Hom.lean

style: remove all isolated `where` (#12991)

Modified MulActionHom.ofEq View on Github →

2024-04-05 00:53

Mathlib/GroupTheory/GroupAction/Hom.lean

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

Added MulActionHom.ofEq View on Github →