mk_eq_mk_of_basis

dimension theorem

dim_range_add_dim_ker

rank-nullity theorem

dim_add_dim_split

This is mostly an auxiliary lemma for dim_sup_add_dim_inf_eq

linear_equiv.dim_eq_lift

Version of linear_equiv.dim_eq without universe constraints.