Commit 2026-06-10 03:47 1ccad003

feat(Topology/Algebra): use Is*Apply for ContinuousLinearMap (#39637) This is the first in many PRs that use the new Is*Apply classes instead of structure specific foo_apply lemmas. The main bulk of the PR is in Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Basic.lean, everything else is just fixing errors. For each foo in zero, one, add, sub, neg, smul` we do the following:

• add an instance IsFooApply
• rename coe_foo to toLinearMap_foo
• depreprecate coe_foo, coe_foo', and foo_apply We are rather conservative when it comes to the instances, in future PRs this will be used more. For consistency, the same renaming has been applied to the comp variants. This resulted in a test being changed.