mathlib

fc66d88c - refactor(ring_theory/derivation): use weaker TC assumptions (#10952)

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.