Commit 2025-02-17 19:42 a1a5f202
View on Github →chore(Algebra/Group/Action): move smul-as-function to End.lean (#22001)
The definition MulAction.toFun is an ingredient in defining scalar actions as endomorphisms of various functions. If we remove it from the Defs file, that saves a relatively large amount of imports since Actions.Defs has few imports already.