mathlib

a283e17b - feat(algebra/module/submodule_pointwise): pointwise negation (#12405)

feat(algebra/module/submodule_pointwise): pointwise negation (#12405) We already have pointwise negation on `add_submonoid`s (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_submonoid`s Finally, we provide a `has_distrib_neg` instance; even though the negation is not cancellative, it does distribute over multiplication as expected.