Commit 2021-05-30 04:33 e2168e55

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