Documentation

Mathlib.Data.Matrix.ColumnRowPartitioned

Block Matrices from Rows and Columns #

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 = fromCols 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

Tags #

column matrices, row matrices, column row block matrices

source
def Matrix.fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
Matrix (m₁ ⊕ m₂) n R

Concatenate together two matrices A₁[m₁ × N] and A₂[m₂ × N] with the same columns (N) to get a bigger matrix indexed by [(m₁ ⊕ m₂) × N]

Equations
  • A₁.fromRows A₂ = Matrix.of (Sum.elim A₁ A₂)
Instances For
    source
    def Matrix.fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
    Matrix m (n₁ ⊕ n₂) R

    Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]

    Equations
    • B₁.fromCols B₂ = Matrix.of fun (i : m) => Sum.elim (B₁ i) (B₂ i)
    Instances For
      source
      def Matrix.toCols₁ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
      Matrix m n₁ R

      Given a column partitioned matrix extract the first column

      Equations
      • A.toCols₁ = Matrix.of fun (i : m) (j : n₁) => A i (Sum.inl j)
      Instances For
        source
        def Matrix.toCols₂ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
        Matrix m n₂ R

        Given a column partitioned matrix extract the second column

        Equations
        • A.toCols₂ = Matrix.of fun (i : m) (j : n₂) => A i (Sum.inr j)
        Instances For
          source
          def Matrix.toRows₁ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :
          Matrix m₁ n R

          Given a row partitioned matrix extract the first row

          Equations
          • A.toRows₁ = Matrix.of fun (i : m₁) (j : n) => A (Sum.inl i) j
          Instances For
            source
            def Matrix.toRows₂ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :
            Matrix m₂ n R

            Given a row partitioned matrix extract the second row

            Equations
            • A.toRows₂ = Matrix.of fun (i : m₂) (j : n) => A (Sum.inr i) j
            Instances For
              source
              @[deprecated Matrix.fromCols]
              def Matrix.fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
              Matrix m (n₁ ⊕ n₂) R

              Alias of Matrix.fromCols.

              Concatenate together two matrices B₁[m × n₁] and B₂[m × n₂] with the same rows (M) to get a bigger matrix indexed by [m × (n₁ ⊕ n₂)]

              Equations
              Instances For
                source
                @[deprecated Matrix.toCols₁]
                def Matrix.toColumns₁ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
                Matrix m n₁ R

                Alias of Matrix.toCols₁.

                Given a column partitioned matrix extract the first column

                Equations
                Instances For
                  source
                  @[deprecated Matrix.toCols₂]
                  def Matrix.toColumns₂ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
                  Matrix m n₂ R

                  Alias of Matrix.toCols₂.

                  Given a column partitioned matrix extract the second column

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Matrix.fromRows_apply_inl {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₁) (j : n) :
                    A₁.fromRows A₂ (Sum.inl i) j = A₁ i j
                    source
                    @[simp]
                    theorem Matrix.fromRows_apply_inr {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (i : m₂) (j : n) :
                    A₁.fromRows A₂ (Sum.inr i) j = A₂ i j
                    source
                    @[simp]
                    theorem Matrix.fromCols_apply_inl {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :
                    A₁.fromCols A₂ i (Sum.inl j) = A₁ i j
                    source
                    @[deprecated Matrix.fromCols_apply_inl]
                    theorem Matrix.fromColumns_apply_inl {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₁) :
                    A₁.fromCols A₂ i (Sum.inl j) = A₁ i j

                    Alias of Matrix.fromCols_apply_inl.

                    source
                    @[simp]
                    theorem Matrix.fromCols_apply_inr {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :
                    A₁.fromCols A₂ i (Sum.inr j) = A₂ i j
                    source
                    @[deprecated Matrix.fromCols_apply_inr]
                    theorem Matrix.fromColumns_apply_inr {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (i : m) (j : n₂) :
                    A₁.fromCols A₂ i (Sum.inr j) = A₂ i j

                    Alias of Matrix.fromCols_apply_inr.

                    source
                    @[simp]
                    theorem Matrix.toRows₁_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₁) (j : n) :
                    A.toRows₁ i j = A (Sum.inl i) j
                    source
                    @[simp]
                    theorem Matrix.toRows₂_apply {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) (i : m₂) (j : n) :
                    A.toRows₂ i j = A (Sum.inr i) j
                    source
                    @[simp]
                    theorem Matrix.toRows₁_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
                    (A₁.fromRows A₂).toRows₁ = A₁
                    source
                    @[simp]
                    theorem Matrix.toRows₂_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
                    (A₁.fromRows A₂).toRows₂ = A₂
                    source
                    @[simp]
                    theorem Matrix.toCols₁_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁) :
                    A.toCols₁ i j = A i (Sum.inl j)
                    source
                    @[deprecated Matrix.toCols₁_apply]
                    theorem Matrix.toColumns₁_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₁) :
                    A.toCols₁ i j = A i (Sum.inl j)

                    Alias of Matrix.toCols₁_apply.

                    source
                    @[simp]
                    theorem Matrix.toCols₂_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) :
                    A.toCols₂ i j = A i (Sum.inr j)
                    source
                    @[deprecated Matrix.toCols₂_apply]
                    theorem Matrix.toColumns₂_apply {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) (i : m) (j : n₂) :
                    A.toCols₂ i j = A i (Sum.inr j)

                    Alias of Matrix.toCols₂_apply.

                    source
                    @[simp]
                    theorem Matrix.toCols₁_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).toCols₁ = A₁
                    source
                    @[deprecated Matrix.toCols₁_fromCols]
                    theorem Matrix.toColumns₁_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).toCols₁ = A₁

                    Alias of Matrix.toCols₁_fromCols.

                    source
                    @[simp]
                    theorem Matrix.toCols₂_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).toCols₂ = A₂
                    source
                    @[deprecated Matrix.toCols₂_fromCols]
                    theorem Matrix.toColumns₂_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).toCols₂ = A₂

                    Alias of Matrix.toCols₂_fromCols.

                    source
                    @[simp]
                    theorem Matrix.fromCols_toCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
                    A.toCols₁.fromCols A.toCols₂ = A
                    source
                    @[deprecated Matrix.fromCols_toCols]
                    theorem Matrix.fromColumns_toColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A : Matrix m (n₁ ⊕ n₂) R) :
                    A.toCols₁.fromCols A.toCols₂ = A

                    Alias of Matrix.fromCols_toCols.

                    source
                    @[simp]
                    theorem Matrix.fromRows_toRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A : Matrix (m₁ ⊕ m₂) n R) :
                    A.toRows₁.fromRows A.toRows₂ = A
                    source
                    theorem Matrix.fromRows_inj {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} :
                    Function.Injective2 Matrix.fromRows
                    source
                    theorem Matrix.fromCols_inj {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} :
                    Function.Injective2 Matrix.fromCols
                    source
                    @[deprecated Matrix.fromCols_inj]
                    theorem Matrix.fromColumns_inj {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} :
                    Function.Injective2 Matrix.fromCols

                    Alias of Matrix.fromCols_inj.

                    source
                    theorem Matrix.fromCols_ext_iff {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
                    A₁.fromCols A₂ = B₁.fromCols B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
                    source
                    @[deprecated Matrix.fromCols_ext_iff]
                    theorem Matrix.fromColumns_ext_iff {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) :
                    A₁.fromCols A₂ = B₁.fromCols B₂ ↔ A₁ = B₁ ∧ A₂ = B₂

                    Alias of Matrix.fromCols_ext_iff.

                    source
                    theorem Matrix.fromRows_ext_iff {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) :
                    A₁.fromRows A₂ = B₁.fromRows B₂ ↔ A₁ = B₁ ∧ A₂ = B₂
                    source
                    theorem Matrix.transpose_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).transpose = A₁.transpose.fromRows A₂.transpose

                    A column partitioned matrix when transposed gives a row partitioned matrix with columns of the initial matrix transposed to become rows.

                    source
                    @[deprecated Matrix.transpose_fromCols]
                    theorem Matrix.transpose_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).transpose = A₁.transpose.fromRows A₂.transpose

                    Alias of Matrix.transpose_fromCols.

                    A column partitioned matrix when transposed gives a row partitioned matrix with columns of the initial matrix transposed to become rows.

                    source
                    theorem Matrix.transpose_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
                    (A₁.fromRows A₂).transpose = A₁.transpose.fromCols A₂.transpose

                    A row partitioned matrix when transposed gives a column partitioned matrix with rows of the initial matrix transposed to become columns.

                    source
                    @[simp]
                    theorem Matrix.fromRows_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
                    -A₁.fromRows A₂ = (-A₁).fromRows (-A₂)

                    Negating a matrix partitioned by rows is equivalent to negating each of the rows.

                    source
                    @[simp]
                    theorem Matrix.fromCols_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :
                    -A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

                    Negating a matrix partitioned by columns is equivalent to negating each of the columns.

                    source
                    @[deprecated Matrix.fromCols_neg]
                    theorem Matrix.fromColumns_neg {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Neg R] (A₁ : Matrix n m₁ R) (A₂ : Matrix n m₂ R) :
                    -A₁.fromCols A₂ = (-A₁).fromCols (-A₂)

                    Alias of Matrix.fromCols_neg.

                    Negating a matrix partitioned by columns is equivalent to negating each of the columns.

                    source
                    @[simp]
                    theorem Matrix.fromCols_fromRows_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
                    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
                    source
                    @[deprecated Matrix.fromCols_fromRows_eq_fromBlocks]
                    theorem Matrix.fromColumns_fromRows_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
                    (B₁₁.fromRows B₂₁).fromCols (B₁₂.fromRows B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

                    Alias of Matrix.fromCols_fromRows_eq_fromBlocks.

                    source
                    @[simp]
                    theorem Matrix.fromRows_fromCols_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
                    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂
                    source
                    @[deprecated Matrix.fromRows_fromCols_eq_fromBlocks]
                    theorem Matrix.fromRows_fromColumn_eq_fromBlocks {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
                    (B₁₁.fromCols B₁₂).fromRows (B₂₁.fromCols B₂₂) = Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂

                    Alias of Matrix.fromRows_fromCols_eq_fromBlocks.

                    source
                    @[simp]
                    theorem Matrix.fromRows_mulVec {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (v : n → R) :
                    (A₁.fromRows A₂).mulVec v = Sum.elim (A₁.mulVec v) (A₂.mulVec v)
                    source
                    @[simp]
                    theorem Matrix.vecMul_fromCols {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
                    Matrix.vecMul v (B₁.fromCols B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)
                    source
                    @[deprecated Matrix.vecMul_fromCols]
                    theorem Matrix.vecMul_fromColumns {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m] (B₁ : Matrix m n₁ R) (B₂ : Matrix m n₂ R) (v : m → R) :
                    Matrix.vecMul v (B₁.fromCols B₂) = Sum.elim (Matrix.vecMul v B₁) (Matrix.vecMul v B₂)

                    Alias of Matrix.vecMul_fromCols.

                    source
                    @[simp]
                    theorem Matrix.sum_elim_vecMul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype m₁] [Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁ → R) (v₂ : m₂ → R) :
                    Matrix.vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = Matrix.vecMul v₁ B₁ + Matrix.vecMul v₂ B₂
                    source
                    @[simp]
                    theorem Matrix.fromCols_mulVec_sum_elim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :
                    (A₁.fromCols A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂
                    source
                    @[deprecated Matrix.fromCols_mulVec_sum_elim]
                    theorem Matrix.fromColumns_mulVec_sum_elim {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (v₁ : n₁ → R) (v₂ : n₂ → R) :
                    (A₁.fromCols A₂).mulVec (Sum.elim v₁ v₂) = A₁.mulVec v₁ + A₂.mulVec v₂

                    Alias of Matrix.fromCols_mulVec_sum_elim.

                    source
                    @[simp]
                    theorem Matrix.fromRows_mul {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B : Matrix n m R) :
                    A₁.fromRows A₂ * B = (A₁ * B).fromRows (A₂ * B)
                    source
                    @[simp]
                    theorem Matrix.mul_fromCols {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
                    A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)
                    source
                    @[deprecated Matrix.mul_fromCols]
                    theorem Matrix.mul_fromColumns {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A : Matrix m n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
                    A * B₁.fromCols B₂ = (A * B₁).fromCols (A * B₂)

                    Alias of Matrix.mul_fromCols.

                    source
                    @[simp]
                    theorem Matrix.fromRows_zero {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Semiring R] :
                    Matrix.fromRows 0 0 = 0
                    source
                    @[simp]
                    theorem Matrix.fromCols_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] :
                    Matrix.fromCols 0 0 = 0
                    source
                    @[deprecated Matrix.fromCols_zero]
                    theorem Matrix.fromColumns_zero {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] :
                    Matrix.fromCols 0 0 = 0

                    Alias of Matrix.fromCols_zero.

                    source
                    theorem Matrix.fromRows_mul_fromCols {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
                    A₁.fromRows A₂ * B₁.fromCols B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

                    A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block matrix.

                    source
                    @[deprecated Matrix.fromRows_mul_fromCols]
                    theorem Matrix.fromRows_mul_fromColumns {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) (B₁ : Matrix n n₁ R) (B₂ : Matrix n n₂ R) :
                    A₁.fromRows A₂ * B₁.fromCols B₂ = Matrix.fromBlocks (A₁ * B₁) (A₁ * B₂) (A₂ * B₁) (A₂ * B₂)

                    Alias of Matrix.fromRows_mul_fromCols.

                    A row partitioned matrix multiplied by a column partitioned matrix gives a 2 by 2 block matrix.

                    source
                    theorem Matrix.fromCols_mul_fromRows {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
                    A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

                    A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer" products of the block matrices.

                    source
                    @[deprecated Matrix.fromCols_mul_fromRows]
                    theorem Matrix.fromColumns_mul_fromRows {R : Type u_1} {m : Type u_2} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
                    A₁.fromCols A₂ * B₁.fromRows B₂ = A₁ * B₁ + A₂ * B₂

                    Alias of Matrix.fromCols_mul_fromRows.

                    A column partitioned matrix multiplied by a row partitioned matrix gives the sum of the "outer" products of the block matrices.

                    source
                    theorem Matrix.fromCols_mul_fromBlocks {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
                    A₁.fromCols A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

                    A column partitioned matrix multipiled by a block matrix results in a column partitioned matrix.

                    source
                    @[deprecated Matrix.fromCols_mul_fromBlocks]
                    theorem Matrix.fromColumns_mul_fromBlocks {R : Type u_1} {m : Type u_2} {m₁ : Type u_3} {m₂ : Type u_4} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype m₁] [Fintype m₂] (A₁ : Matrix m m₁ R) (A₂ : Matrix m m₂ R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
                    A₁.fromCols A₂ * Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ = (A₁ * B₁₁ + A₂ * B₂₁).fromCols (A₁ * B₁₂ + A₂ * B₂₂)

                    Alias of Matrix.fromCols_mul_fromBlocks.

                    A column partitioned matrix multipiled by a block matrix results in a column partitioned matrix.

                    source
                    theorem Matrix.fromBlocks_mul_fromRows {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [Semiring R] [Fintype n₁] [Fintype n₂] (A₁ : Matrix n₁ n R) (A₂ : Matrix n₂ n R) (B₁₁ : Matrix m₁ n₁ R) (B₁₂ : Matrix m₁ n₂ R) (B₂₁ : Matrix m₂ n₁ R) (B₂₂ : Matrix m₂ n₂ R) :
                    Matrix.fromBlocks B₁₁ B₁₂ B₂₁ B₂₂ * A₁.fromRows A₂ = (B₁₁ * A₁ + B₁₂ * A₂).fromRows (B₂₁ * A₁ + B₂₂ * A₂)

                    A block matrix multiplied by a row partitioned matrix gives a row partitioned matrix.

                    source
                    theorem Matrix.fromCols_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [CommRing R] [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂] (e : n ≃ n₁ ⊕ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
                    A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

                    Multiplication of a matrix by its inverse is commutative. This is the column and row partitioned matrix form of Matrix.mul_eq_one_comm.

                    The condition e : n ≃ n₁ ⊕ n₂ states that fromCols A₁ A₂ and fromRows B₁ B₂ are "square".

                    source
                    @[deprecated Matrix.fromCols_mul_fromRows_eq_one_comm]
                    theorem Matrix.fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} {n₁ : Type u_6} {n₂ : Type u_7} [CommRing R] [Fintype n₁] [Fintype n₂] [Fintype n] [DecidableEq n] [DecidableEq n₁] [DecidableEq n₂] (e : n ≃ n₁ ⊕ n₂) (A₁ : Matrix n n₁ R) (A₂ : Matrix n n₂ R) (B₁ : Matrix n₁ n R) (B₂ : Matrix n₂ n R) :
                    A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

                    Alias of Matrix.fromCols_mul_fromRows_eq_one_comm.

                    Multiplication of a matrix by its inverse is commutative. This is the column and row partitioned matrix form of Matrix.mul_eq_one_comm.

                    The condition e : n ≃ n₁ ⊕ n₂ states that fromCols A₁ A₂ and fromRows B₁ B₂ are "square".

                    source
                    theorem Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} [CommRing R] [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p] (A₁ : Matrix n { i : n // p i } R) (A₂ : Matrix n { i : n // ¬p i } R) (B₁ : Matrix { i : n // p i } n R) (B₂ : Matrix { i : n // ¬p i } n R) :
                    A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

                    The lemma fromCols_mul_fromRows_eq_one_comm specialized to the case where the index sets n₁ and n₂, are the result of subtyping by a predicate and its complement.

                    source
                    @[deprecated Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm]
                    theorem Matrix.equiv_compl_fromColumns_mul_fromRows_eq_one_comm {R : Type u_1} {n : Type u_5} [CommRing R] [Fintype n] [DecidableEq n] (p : n → Prop) [DecidablePred p] (A₁ : Matrix n { i : n // p i } R) (A₂ : Matrix n { i : n // ¬p i } R) (B₁ : Matrix { i : n // p i } n R) (B₂ : Matrix { i : n // ¬p i } n R) :
                    A₁.fromCols A₂ * B₁.fromRows B₂ = 1 ↔ B₁.fromRows B₂ * A₁.fromCols A₂ = 1

                    Alias of Matrix.equiv_compl_fromCols_mul_fromRows_eq_one_comm.

                    The lemma fromCols_mul_fromRows_eq_one_comm specialized to the case where the index sets n₁ and n₂, are the result of subtyping by a predicate and its complement.

                    source
                    theorem Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Star R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose

                    A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned matrix with the columns of the initial matrix conjugate transposed to become rows.

                    source
                    @[deprecated Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose]
                    theorem Matrix.conjTranspose_fromColumns_eq_fromRows_conjTranspose {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} [Star R] (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R) :
                    (A₁.fromCols A₂).conjTranspose = A₁.conjTranspose.fromRows A₂.conjTranspose

                    Alias of Matrix.conjTranspose_fromCols_eq_fromRows_conjTranspose.

                    A column partitioned matrix in a Star ring when conjugate transposed gives a row partitioned matrix with the columns of the initial matrix conjugate transposed to become rows.

                    source
                    theorem Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Star R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
                    (A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromCols A₂.conjTranspose

                    A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix with the rows of the initial matrix conjugate transposed to become columns.

                    source
                    @[deprecated Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose]
                    theorem Matrix.conjTranspose_fromRows_eq_fromColumns_conjTranspose {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [Star R] (A₁ : Matrix m₁ n R) (A₂ : Matrix m₂ n R) :
                    (A₁.fromRows A₂).conjTranspose = A₁.conjTranspose.fromCols A₂.conjTranspose

                    Alias of Matrix.conjTranspose_fromRows_eq_fromCols_conjTranspose.

                    A row partitioned matrix in a Star ring when conjugate transposed gives a column partitioned matrix with the rows of the initial matrix conjugate transposed to become columns.