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.

Estimated changes

Modified src/geometry/manifold/algebra/left_invariant_derivation.lean

Modified src/geometry/manifold/derivation_bundle.lean

Modified src/ring_theory/derivation.lean

deleted theorem derivation.Rsmul_apply

deleted theorem derivation.coe_Rsmul

deleted theorem derivation.coe_Rsmul_linear_map

added theorem derivation.coe_mk'

added theorem derivation.coe_mk'_linear_map

modified theorem derivation.coe_smul

modified theorem derivation.coe_smul_linear_map

modified theorem derivation.map_one_eq_zero

added def derivation.mk'

modified theorem derivation.mk_coe

modified theorem derivation.smul_apply