# Commit 2021-12-21 23:32 fc66d88c

View on Github →refactor(ring_theory/derivation): use weaker TC assumptions (#10952)
Don't assume `[add_cancel_comm_monoid M]`

, add `map_one_eq_zero`

as an axiom instead. Add a constructor `derivation.mk'`

that deduces `map_one_eq_zero`

from `leibniz`

.
Also generalize `smul`

/`module`

instances.