Commit 2020-10-21 13:35 75316cad
View on Github →chore(linear_algebra/basic): a few simp lemmas (#4727)
- add
submodule.nonempty; - add
@[simp]tosubmodule.map_id; - add
submodule.neg_coe,protected submodule.map_neg, andsubmodule.span_neg.
chore(linear_algebra/basic): a few simp lemmas (#4727)
submodule.nonempty;@[simp] to submodule.map_id;submodule.neg_coe, protected submodule.map_neg, and submodule.span_neg.