Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-26 13:34 fa27c0c0

View on Github →

feat(ring_theory/derivation): define push forward of derivations (#7715)

Estimated changes

added theorem derivation.coe_comp
added def derivation.comp
added theorem derivation.mk_coe