Mathlib v3 is deprecated. Go to Mathlib v4

Def derivation.comp

Modification history

2021-05-30 04:33
src/ring_theory/derivation.lean
feat(src/ring_theory/derivation): merge duplicates `derivation.comp` and `linear_map.comp_der` (#7727) …
Deleted derivation.compView on Github →
2021-05-26 13:34
src/ring_theory/derivation.lean
feat(ring_theory/derivation): define push forward of derivations (#7715)
Added derivation.compView on Github →