Commit 2021-06-21 14:25 eb13f6b7

feat(ring_theory/derivation): add missing dsimp lemmas, use old_structure_command, golf structure proofs (#8013) This adds a pile of missing coercion lemmas proved by refl, and uses them to construct the add_comm_monoid, add_comm_group, and module instances. This also changes derivation to be an old-style structure, which is more in line with the other bundled homomorphisms. This also removes derivation.commutator to avoid having two ways to spell the same thing, as this leads to lemmas being harder to apply