mathlib3

chore(linear_algebra/basic): simplify two proofs

#2123

Merged