mathlib

75316cad - chore(linear_algebra/basic): a few simp lemmas (#4727)

chore(linear_algebra/basic): a few simp lemmas (#4727) * add `submodule.nonempty`; * add `@[simp]` to `submodule.map_id`; * add `submodule.neg_coe`, `protected submodule.map_neg`, and `submodule.span_neg`.