mathlib

bb52355b - feat(linear_algebra/basic): define `linear_equiv.neg` (#4749)

feat(linear_algebra/basic): define `linear_equiv.neg` (#4749) Also weaken requirements for `has_neg (M →ₗ[R] M₂)` from `[add_comm_group M]` `[add_comm_group M₂]` to `[add_comm_monoid M]` `[add_comm_group M₂]`.