Commit 2022-03-02 18:33 a283e17b

feat(algebra/module/submodule_pointwise): pointwise negation (#12405) We already have pointwise negation on add_submonoids (from #10451), this extends it to submodules. The lemmas are all copies of the add_submonoid lemmas, except for two new lemmas:

• submodule.neg_to_add_submonoid
• submodule.neg_eq_self, which isn't true for add_submonoids Finally, we provide a has_distrib_neg instance; even though the negation is not cancellative, it does distribute over multiplication as expected.