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.