mathlib

e2168e55 - feat(src/ring_theory/derivation): merge duplicates `derivation.comp` and `linear_map.comp_der` (#7727)

feat(src/ring_theory/derivation): merge duplicates `derivation.comp` and `linear_map.comp_der` (#7727) I propose keeping the version introduced in #7715 since it also contains the statement that the push forward is linear, but moving it to the `linear_map` namespace to enable dot notation. Thanks to @Nicknamen for alerting me to the duplication: https://github.com/leanprover-community/mathlib/pull/7715#issuecomment-849192370