Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.comp_der_apply

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 linear_map.comp_der_applyView on Github →
2020-08-16 20:46
src/ring_theory/derivation.lean
feat(ring_theory/derivations): stab on derivations (#3688)
Added linear_map.comp_der_applyView on Github →