feat(data/matrix/basic): more lemmas about submatrix (#18738)
This adds trivial results about reordering rows and columns in a matrix:
* Reordering can be moved around `dot_product`, `mul_vec`, and `vec_mul` (previouly we only had `mul`)
* Reordering can be moved through `adjugate`
* Reordering can be moved through row and column updates.
* Reordering can be moved through `to_lin'`
* Reordering does not affect `matrix.rank`
Also adds some missing `of` wrappers.
Lemmas about reindexing are useful when working with block matrices, as they make it possible to make symmetry arguments.
