Commit 2023-08-02 13:41 b36a2c75

feat: column and row partitioned matrices (#6052) This file provides the basic definitions of matrices composed from columns and rows. The concatenation of two matrices with the same row indices can be expressed as A = fromColumns A₁ A₂ the concatenation of two matrices with the same column indices can be expressed as B = fromRows B₁ B₂. We then provide a few lemmas that deal with the products of these with each other and with block matrices. Two particular lemmas fromColumns_mul_fromRows_eq_one_comm and equiv_compl_fromColumns_mul_fromRows_eq_one_comm deal with the case of matrix multiplication that gives one as a result. This gives a crude (but usable) replacement for the Invertible type which can only be applied to square matrices (with the same index type for rows and columns).