mathlib3

32642e17 - feat(linear_algebra): add dim_sup_add_dim_inf_eq