Commit 2026-05-21 01:59 89d44072

feat(Data/FunLike): introduce typeclasses for algebraic properties of FunLike (#37779) These typeclasses remove the need for each function space that has, e.g., a linear structure to define add_apply, smul_apply, etc. Instead after defining the the Add instance one also defines a FunLikeAdd instance (with a proof usually being rfl). Allows removing some boilerplate as theorems like sum_apply are currently proved in various files: after this PR, they can be proved in an abstract way. Moreover, we provide abbreviations for further structure (such as `Semigroup``) in the concrete function spaces. The usage of these typeclasses were prototyped in #33477 and will be merged in a separate PR. The docstrings were generated with AI (and heavily edited afterwards), everything else is handwritten.