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.

Estimated changes