Documentation

Mathlib.Data.Matrix.Block

Block Matrices #

Main definitions #

theorem Matrix.dotProduct_block {m : Type u_2} {n : Type u_3} {α : Type u_12} [Fintype m] [Fintype n] [Mul α] [AddCommMonoid α] (v : m nα) (w : m nα) :
Matrix.dotProduct v w = Matrix.dotProduct (v Sum.inl) (w Sum.inl) + Matrix.dotProduct (v Sum.inr) (w Sum.inr)
def Matrix.fromBlocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
Matrix (n o) (l m) α

We can form a single large matrix by flattening smaller 'block' matrices of compatible dimensions.

Equations
Instances For
    @[simp]
    theorem Matrix.fromBlocks_apply₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : n) (j : l) :
    Matrix.fromBlocks A B C D (Sum.inl i) (Sum.inl j) = A i j
    @[simp]
    theorem Matrix.fromBlocks_apply₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : n) (j : m) :
    Matrix.fromBlocks A B C D (Sum.inl i) (Sum.inr j) = B i j
    @[simp]
    theorem Matrix.fromBlocks_apply₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : o) (j : l) :
    Matrix.fromBlocks A B C D (Sum.inr i) (Sum.inl j) = C i j
    @[simp]
    theorem Matrix.fromBlocks_apply₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (i : o) (j : m) :
    Matrix.fromBlocks A B C D (Sum.inr i) (Sum.inr j) = D i j
    def Matrix.toBlocks₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
    Matrix n l α

    Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top left" submatrix.

    Equations
    • M.toBlocks₁₁ = Matrix.of fun (i : n) (j : l) => M (Sum.inl i) (Sum.inl j)
    Instances For
      def Matrix.toBlocks₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
      Matrix n m α

      Given a matrix whose row and column indexes are sum types, we can extract the corresponding "top right" submatrix.

      Equations
      • M.toBlocks₁₂ = Matrix.of fun (i : n) (j : m) => M (Sum.inl i) (Sum.inr j)
      Instances For
        def Matrix.toBlocks₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
        Matrix o l α

        Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom left" submatrix.

        Equations
        • M.toBlocks₂₁ = Matrix.of fun (i : o) (j : l) => M (Sum.inr i) (Sum.inl j)
        Instances For
          def Matrix.toBlocks₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
          Matrix o m α

          Given a matrix whose row and column indexes are sum types, we can extract the corresponding "bottom right" submatrix.

          Equations
          • M.toBlocks₂₂ = Matrix.of fun (i : o) (j : m) => M (Sum.inr i) (Sum.inr j)
          Instances For
            theorem Matrix.fromBlocks_toBlocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (n o) (l m) α) :
            Matrix.fromBlocks M.toBlocks₁₁ M.toBlocks₁₂ M.toBlocks₂₁ M.toBlocks₂₂ = M
            @[simp]
            theorem Matrix.toBlocks_fromBlocks₁₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
            (Matrix.fromBlocks A B C D).toBlocks₁₁ = A
            @[simp]
            theorem Matrix.toBlocks_fromBlocks₁₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
            (Matrix.fromBlocks A B C D).toBlocks₁₂ = B
            @[simp]
            theorem Matrix.toBlocks_fromBlocks₂₁ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
            (Matrix.fromBlocks A B C D).toBlocks₂₁ = C
            @[simp]
            theorem Matrix.toBlocks_fromBlocks₂₂ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
            (Matrix.fromBlocks A B C D).toBlocks₂₂ = D
            theorem Matrix.ext_iff_blocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {A : Matrix (n o) (l m) α} {B : Matrix (n o) (l m) α} :
            A = B A.toBlocks₁₁ = B.toBlocks₁₁ A.toBlocks₁₂ = B.toBlocks₁₂ A.toBlocks₂₁ = B.toBlocks₂₁ A.toBlocks₂₂ = B.toBlocks₂₂

            Two block matrices are equal if their blocks are equal.

            @[simp]
            theorem Matrix.fromBlocks_inj {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {A : Matrix n l α} {B : Matrix n m α} {C : Matrix o l α} {D : Matrix o m α} {A' : Matrix n l α} {B' : Matrix n m α} {C' : Matrix o l α} {D' : Matrix o m α} :
            Matrix.fromBlocks A B C D = Matrix.fromBlocks A' B' C' D' A = A' B = B' C = C' D = D'
            theorem Matrix.fromBlocks_map {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : αβ) :
            (Matrix.fromBlocks A B C D).map f = Matrix.fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)
            theorem Matrix.fromBlocks_transpose {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
            (Matrix.fromBlocks A B C D).transpose = Matrix.fromBlocks A.transpose C.transpose B.transpose D.transpose
            theorem Matrix.fromBlocks_conjTranspose {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Star α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
            (Matrix.fromBlocks A B C D).conjTranspose = Matrix.fromBlocks A.conjTranspose C.conjTranspose B.conjTranspose D.conjTranspose
            @[simp]
            theorem Matrix.fromBlocks_submatrix_sum_swap_left {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : pl m) :
            (Matrix.fromBlocks A B C D).submatrix Sum.swap f = (Matrix.fromBlocks C D A B).submatrix id f
            @[simp]
            theorem Matrix.fromBlocks_submatrix_sum_swap_right {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : pn o) :
            (Matrix.fromBlocks A B C D).submatrix f Sum.swap = (Matrix.fromBlocks B A D C).submatrix f id
            theorem Matrix.fromBlocks_submatrix_sum_swap_sum_swap {l : Type u_14} {m : Type u_15} {n : Type u_16} {o : Type u_17} {α : Type u_18} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
            (Matrix.fromBlocks A B C D).submatrix Sum.swap Sum.swap = Matrix.fromBlocks D C B A
            def Matrix.IsTwoBlockDiagonal {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] (A : Matrix (n o) (l m) α) :

            A 2x2 block matrix is block diagonal if the blocks outside of the diagonal vanish

            Equations
            • A.IsTwoBlockDiagonal = (A.toBlocks₁₂ = 0 A.toBlocks₂₁ = 0)
            Instances For
              def Matrix.toBlock {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : Matrix m n α) (p : mProp) (q : nProp) :
              Matrix { a : m // p a } { a : n // q a } α

              Let p pick out certain rows and q pick out certain columns of a matrix M. Then toBlock M p q is the corresponding block matrix.

              Equations
              • M.toBlock p q = M.submatrix Subtype.val Subtype.val
              Instances For
                @[simp]
                theorem Matrix.toBlock_apply {m : Type u_2} {n : Type u_3} {α : Type u_12} (M : Matrix m n α) (p : mProp) (q : nProp) (i : { a : m // p a }) (j : { a : n // q a }) :
                M.toBlock p q i j = M i j
                def Matrix.toSquareBlockProp {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : mProp) :
                Matrix { a : m // p a } { a : m // p a } α

                Let p pick out certain rows and columns of a square matrix M. Then toSquareBlockProp M p is the corresponding block matrix.

                Equations
                • M.toSquareBlockProp p = M.toBlock p p
                Instances For
                  theorem Matrix.toSquareBlockProp_def {m : Type u_2} {α : Type u_12} (M : Matrix m m α) (p : mProp) :
                  M.toSquareBlockProp p = Matrix.of fun (i j : { a : m // p a }) => M i j
                  def Matrix.toSquareBlock {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : Matrix m m α) (b : mβ) (k : β) :
                  Matrix { a : m // b a = k } { a : m // b a = k } α

                  Let b map rows and columns of a square matrix M to blocks. Then toSquareBlock M b k is the block k matrix.

                  Equations
                  • M.toSquareBlock b k = M.toSquareBlockProp fun (a : m) => b a = k
                  Instances For
                    theorem Matrix.toSquareBlock_def {m : Type u_2} {α : Type u_12} {β : Type u_13} (M : Matrix m m α) (b : mβ) (k : β) :
                    M.toSquareBlock b k = Matrix.of fun (i j : { a : m // b a = k }) => M i j
                    theorem Matrix.fromBlocks_smul {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_10} {α : Type u_12} [SMul R α] (x : R) (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) :
                    x Matrix.fromBlocks A B C D = Matrix.fromBlocks (x A) (x B) (x C) (x D)
                    theorem Matrix.fromBlocks_neg {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {R : Type u_10} [Neg R] (A : Matrix n l R) (B : Matrix n m R) (C : Matrix o l R) (D : Matrix o m R) :
                    @[simp]
                    theorem Matrix.fromBlocks_zero {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] :
                    theorem Matrix.fromBlocks_add {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Add α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix n l α) (B' : Matrix n m α) (C' : Matrix o l α) (D' : Matrix o m α) :
                    Matrix.fromBlocks A B C D + Matrix.fromBlocks A' B' C' D' = Matrix.fromBlocks (A + A') (B + B') (C + C') (D + D')
                    theorem Matrix.fromBlocks_multiply {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {q : Type u_6} {α : Type u_12} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix l p α) (B' : Matrix l q α) (C' : Matrix m p α) (D' : Matrix m q α) :
                    Matrix.fromBlocks A B C D * Matrix.fromBlocks A' B' C' D' = Matrix.fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')
                    theorem Matrix.fromBlocks_mulVec {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : l mα) :
                    (Matrix.fromBlocks A B C D).mulVec x = Sum.elim (A.mulVec (x Sum.inl) + B.mulVec (x Sum.inr)) (C.mulVec (x Sum.inl) + D.mulVec (x Sum.inr))
                    theorem Matrix.vecMul_fromBlocks {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (x : n oα) :
                    Matrix.vecMul x (Matrix.fromBlocks A B C D) = Sum.elim (Matrix.vecMul (x Sum.inl) A + Matrix.vecMul (x Sum.inr) C) (Matrix.vecMul (x Sum.inl) B + Matrix.vecMul (x Sum.inr) D)
                    theorem Matrix.toBlock_diagonal_self {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] (d : mα) (p : mProp) :
                    (Matrix.diagonal d).toBlock p p = Matrix.diagonal fun (i : Subtype p) => d i
                    theorem Matrix.toBlock_diagonal_disjoint {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] (d : mα) {p : mProp} {q : mProp} (hpq : Disjoint p q) :
                    (Matrix.diagonal d).toBlock p q = 0
                    @[simp]
                    theorem Matrix.fromBlocks_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (d₁ : lα) (d₂ : mα) :
                    @[simp]
                    theorem Matrix.toBlocks₁₁_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l mα) :
                    (Matrix.diagonal v).toBlocks₁₁ = Matrix.diagonal fun (i : l) => v (Sum.inl i)
                    @[simp]
                    theorem Matrix.toBlocks₂₂_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l mα) :
                    (Matrix.diagonal v).toBlocks₂₂ = Matrix.diagonal fun (i : m) => v (Sum.inr i)
                    @[simp]
                    theorem Matrix.toBlocks₁₂_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l mα) :
                    (Matrix.diagonal v).toBlocks₁₂ = 0
                    @[simp]
                    theorem Matrix.toBlocks₂₁_diagonal {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] (v : l mα) :
                    (Matrix.diagonal v).toBlocks₂₁ = 0
                    @[simp]
                    theorem Matrix.fromBlocks_one {l : Type u_1} {m : Type u_2} {α : Type u_12} [DecidableEq l] [DecidableEq m] [Zero α] [One α] :
                    @[simp]
                    theorem Matrix.toBlock_one_self {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] [One α] (p : mProp) :
                    theorem Matrix.toBlock_one_disjoint {m : Type u_2} {α : Type u_12} [DecidableEq m] [Zero α] [One α] {p : mProp} {q : mProp} (hpq : Disjoint p q) :
                    def Matrix.blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) :
                    Matrix (m × o) (n × o) α

                    Matrix.blockDiagonal M turns a homogenously-indexed collection of matrices M : o → Matrix m n α' into an m × o-by-n × o block matrix which has the entries of M along the diagonal and zero elsewhere.

                    See also Matrix.blockDiagonal' if the matrices may not have the same size everywhere.

                    Equations
                    • Matrix.blockDiagonal M = Matrix.of fun (x : m × o) (x_1 : n × o) => match x with | (i, k) => match x_1 with | (j, k') => if k = k' then M k i j else 0
                    Instances For
                      theorem Matrix.blockDiagonal_apply' {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) (i : m) (k : o) (j : n) (k' : o) :
                      Matrix.blockDiagonal M (i, k) (j, k') = if k = k' then M k i j else 0
                      theorem Matrix.blockDiagonal_apply {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) (ik : m × o) (jk : n × o) :
                      Matrix.blockDiagonal M ik jk = if ik.2 = jk.2 then M ik.2 ik.1 jk.1 else 0
                      @[simp]
                      theorem Matrix.blockDiagonal_apply_eq {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) (i : m) (j : n) (k : o) :
                      Matrix.blockDiagonal M (i, k) (j, k) = M k i j
                      theorem Matrix.blockDiagonal_apply_ne {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) (i : m) (j : n) {k : o} {k' : o} (h : k k') :
                      Matrix.blockDiagonal M (i, k) (j, k') = 0
                      theorem Matrix.blockDiagonal_map {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} [DecidableEq o] [Zero α] [Zero β] (M : oMatrix m n α) (f : αβ) (hf : f 0 = 0) :
                      (Matrix.blockDiagonal M).map f = Matrix.blockDiagonal fun (k : o) => (M k).map f
                      @[simp]
                      theorem Matrix.blockDiagonal_transpose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) :
                      (Matrix.blockDiagonal M).transpose = Matrix.blockDiagonal fun (k : o) => (M k).transpose
                      @[simp]
                      theorem Matrix.blockDiagonal_conjTranspose {m : Type u_2} {n : Type u_3} {o : Type u_4} [DecidableEq o] {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : oMatrix m n α) :
                      (Matrix.blockDiagonal M).conjTranspose = Matrix.blockDiagonal fun (k : o) => (M k).conjTranspose
                      @[simp]
                      theorem Matrix.blockDiagonal_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] :
                      @[simp]
                      theorem Matrix.blockDiagonal_diagonal {m : Type u_2} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] [DecidableEq m] (d : omα) :
                      (Matrix.blockDiagonal fun (k : o) => Matrix.diagonal (d k)) = Matrix.diagonal fun (ik : m × o) => d ik.2 ik.1
                      @[simp]
                      theorem Matrix.blockDiagonal_one {m : Type u_2} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] [DecidableEq m] [One α] :
                      @[simp]
                      theorem Matrix.blockDiagonal_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [AddZeroClass α] (M : oMatrix m n α) (N : oMatrix m n α) :
                      @[simp]
                      theorem Matrix.blockDiagonalAddMonoidHom_apply (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [DecidableEq o] [AddZeroClass α] (M : oMatrix m n α) :
                      def Matrix.blockDiagonalAddMonoidHom (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [DecidableEq o] [AddZeroClass α] :
                      (oMatrix m n α) →+ Matrix (m × o) (n × o) α

                      Matrix.blockDiagonal as an AddMonoidHom.

                      Equations
                      Instances For
                        @[simp]
                        theorem Matrix.blockDiagonal_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [AddGroup α] (M : oMatrix m n α) :
                        @[simp]
                        theorem Matrix.blockDiagonal_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [AddGroup α] (M : oMatrix m n α) (N : oMatrix m n α) :
                        @[simp]
                        theorem Matrix.blockDiagonal_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {p : Type u_5} {α : Type u_12} [DecidableEq o] [Fintype n] [Fintype o] [NonUnitalNonAssocSemiring α] (M : oMatrix m n α) (N : oMatrix n p α) :
                        @[simp]
                        theorem Matrix.blockDiagonalRingHom_apply (m : Type u_2) (o : Type u_4) (α : Type u_12) [DecidableEq o] [DecidableEq m] [Fintype o] [Fintype m] [NonAssocSemiring α] (M : oMatrix m m α) :
                        def Matrix.blockDiagonalRingHom (m : Type u_2) (o : Type u_4) (α : Type u_12) [DecidableEq o] [DecidableEq m] [Fintype o] [Fintype m] [NonAssocSemiring α] :
                        (oMatrix m m α) →+* Matrix (m × o) (m × o) α

                        Matrix.blockDiagonal as a RingHom.

                        Equations
                        Instances For
                          @[simp]
                          theorem Matrix.blockDiagonal_pow {m : Type u_2} {o : Type u_4} {α : Type u_12} [DecidableEq o] [DecidableEq m] [Fintype o] [Fintype m] [Semiring α] (M : oMatrix m m α) (n : ) :
                          @[simp]
                          theorem Matrix.blockDiagonal_smul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] {R : Type u_14} [Monoid R] [AddMonoid α] [DistribMulAction R α] (x : R) (M : oMatrix m n α) :
                          def Matrix.blockDiag {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o) :
                          Matrix m n α

                          Extract a block from the diagonal of a block diagonal matrix.

                          This is the block form of Matrix.diag, and the left-inverse of Matrix.blockDiagonal.

                          Equations
                          • M.blockDiag k = Matrix.of fun (i : m) (j : n) => M (i, k) (j, k)
                          Instances For
                            theorem Matrix.blockDiag_apply {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o) (i : m) (j : n) :
                            M.blockDiag k i j = M (i, k) (j, k)
                            theorem Matrix.blockDiag_map {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (M : Matrix (m × o) (n × o) α) (f : αβ) :
                            (M.map f).blockDiag = fun (k : o) => (M.blockDiag k).map f
                            @[simp]
                            theorem Matrix.blockDiag_transpose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} (M : Matrix (m × o) (n × o) α) (k : o) :
                            M.transpose.blockDiag k = (M.blockDiag k).transpose
                            @[simp]
                            theorem Matrix.blockDiag_conjTranspose {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : Matrix (m × o) (n × o) α) (k : o) :
                            M.conjTranspose.blockDiag k = (M.blockDiag k).conjTranspose
                            @[simp]
                            theorem Matrix.blockDiag_zero {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] :
                            @[simp]
                            theorem Matrix.blockDiag_diagonal {m : Type u_2} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] [DecidableEq m] (d : m × oα) (k : o) :
                            (Matrix.diagonal d).blockDiag k = Matrix.diagonal fun (i : m) => d (i, k)
                            @[simp]
                            theorem Matrix.blockDiag_blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] (M : oMatrix m n α) :
                            (Matrix.blockDiagonal M).blockDiag = M
                            theorem Matrix.blockDiagonal_injective {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] :
                            Function.Injective Matrix.blockDiagonal
                            @[simp]
                            theorem Matrix.blockDiagonal_inj {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] {M : oMatrix m n α} {N : oMatrix m n α} :
                            @[simp]
                            theorem Matrix.blockDiag_one {m : Type u_2} {o : Type u_4} {α : Type u_12} [Zero α] [DecidableEq o] [DecidableEq m] [One α] :
                            @[simp]
                            theorem Matrix.blockDiag_add {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [AddZeroClass α] (M : Matrix (m × o) (n × o) α) (N : Matrix (m × o) (n × o) α) :
                            (M + N).blockDiag = M.blockDiag + N.blockDiag
                            @[simp]
                            theorem Matrix.blockDiagAddMonoidHom_apply (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [AddZeroClass α] (M : Matrix (m × o) (n × o) α) (k : o) :
                            (Matrix.blockDiagAddMonoidHom m n o α) M k = M.blockDiag k
                            def Matrix.blockDiagAddMonoidHom (m : Type u_2) (n : Type u_3) (o : Type u_4) (α : Type u_12) [AddZeroClass α] :
                            Matrix (m × o) (n × o) α →+ oMatrix m n α

                            Matrix.blockDiag as an AddMonoidHom.

                            Equations
                            Instances For
                              @[simp]
                              theorem Matrix.blockDiag_neg {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [AddGroup α] (M : Matrix (m × o) (n × o) α) :
                              (-M).blockDiag = -M.blockDiag
                              @[simp]
                              theorem Matrix.blockDiag_sub {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [AddGroup α] (M : Matrix (m × o) (n × o) α) (N : Matrix (m × o) (n × o) α) :
                              (M - N).blockDiag = M.blockDiag - N.blockDiag
                              @[simp]
                              theorem Matrix.blockDiag_smul {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {R : Type u_14} [Monoid R] [AddMonoid α] [DistribMulAction R α] (x : R) (M : Matrix (m × o) (n × o) α) :
                              (x M).blockDiag = x M.blockDiag
                              def Matrix.blockDiagonal' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) :
                              Matrix ((i : o) × m' i) ((i : o) × n' i) α

                              Matrix.blockDiagonal' M turns M : Π i, Matrix (m i) (n i) α into a Σ i, m i-by-Σ i, n i block matrix which has the entries of M along the diagonal and zero elsewhere.

                              This is the dependently-typed version of Matrix.blockDiagonal.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem Matrix.blockDiagonal'_apply' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (k' : o) (j : n' k') :
                                Matrix.blockDiagonal' M k, i k', j = if h : k = k' then M k i (cast j) else 0
                                theorem Matrix.blockDiagonal'_eq_blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) {k : o} {k' : o} (i : m) (j : n) :
                                Matrix.blockDiagonal M (i, k) (j, k') = Matrix.blockDiagonal' M k, i k', j
                                theorem Matrix.blockDiagonal'_submatrix_eq_blockDiagonal {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [DecidableEq o] [Zero α] (M : oMatrix m n α) :
                                (Matrix.blockDiagonal' M).submatrix (Prod.toSigma Prod.swap) (Prod.toSigma Prod.swap) = Matrix.blockDiagonal M
                                theorem Matrix.blockDiagonal'_apply {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (ik : (i : o) × m' i) (jk : (i : o) × n' i) :
                                Matrix.blockDiagonal' M ik jk = if h : ik.fst = jk.fst then M ik.fst ik.snd (cast jk.snd) else 0
                                @[simp]
                                theorem Matrix.blockDiagonal'_apply_eq {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) (k : o) (i : m' k) (j : n' k) :
                                Matrix.blockDiagonal' M k, i k, j = M k i j
                                theorem Matrix.blockDiagonal'_apply_ne {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) {k : o} {k' : o} (i : m' k) (j : n' k') (h : k k') :
                                Matrix.blockDiagonal' M k, i k', j = 0
                                theorem Matrix.blockDiagonal'_map {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} {β : Type u_13} [DecidableEq o] [Zero α] [Zero β] (M : (i : o) → Matrix (m' i) (n' i) α) (f : αβ) (hf : f 0 = 0) :
                                (Matrix.blockDiagonal' M).map f = Matrix.blockDiagonal' fun (k : o) => (M k).map f
                                @[simp]
                                theorem Matrix.blockDiagonal'_transpose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [Zero α] (M : (i : o) → Matrix (m' i) (n' i) α) :
                                (Matrix.blockDiagonal' M).transpose = Matrix.blockDiagonal' fun (k : o) => (M k).transpose
                                @[simp]
                                theorem Matrix.blockDiagonal'_conjTranspose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} [DecidableEq o] {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : (i : o) → Matrix (m' i) (n' i) α) :
                                (Matrix.blockDiagonal' M).conjTranspose = Matrix.blockDiagonal' fun (k : o) => (M k).conjTranspose
                                @[simp]
                                theorem Matrix.blockDiagonal'_zero {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [Zero α] :
                                @[simp]
                                theorem Matrix.blockDiagonal'_diagonal {o : Type u_4} {m' : oType u_7} {α : Type u_12} [DecidableEq o] [Zero α] [(i : o) → DecidableEq (m' i)] (d : (i : o) → m' iα) :
                                (Matrix.blockDiagonal' fun (k : o) => Matrix.diagonal (d k)) = Matrix.diagonal fun (ik : (i : o) × m' i) => d ik.fst ik.snd
                                @[simp]
                                theorem Matrix.blockDiagonal'_one {o : Type u_4} {m' : oType u_7} {α : Type u_12} [DecidableEq o] [Zero α] [(i : o) → DecidableEq (m' i)] [One α] :
                                @[simp]
                                theorem Matrix.blockDiagonal'_add {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [AddZeroClass α] (M : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (m' i) (n' i) α) :
                                @[simp]
                                theorem Matrix.blockDiagonal'AddMonoidHom_apply {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [DecidableEq o] [AddZeroClass α] (M : (i : o) → Matrix (m' i) (n' i) α) :
                                def Matrix.blockDiagonal'AddMonoidHom {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [DecidableEq o] [AddZeroClass α] :
                                ((i : o) → Matrix (m' i) (n' i) α) →+ Matrix ((i : o) × m' i) ((i : o) × n' i) α

                                Matrix.blockDiagonal' as an AddMonoidHom.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Matrix.blockDiagonal'_neg {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [AddGroup α] (M : (i : o) → Matrix (m' i) (n' i) α) :
                                  @[simp]
                                  theorem Matrix.blockDiagonal'_sub {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] [AddGroup α] (M : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (m' i) (n' i) α) :
                                  @[simp]
                                  theorem Matrix.blockDiagonal'_mul {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {p' : oType u_9} {α : Type u_12} [DecidableEq o] [NonUnitalNonAssocSemiring α] [(i : o) → Fintype (n' i)] [Fintype o] (M : (i : o) → Matrix (m' i) (n' i) α) (N : (i : o) → Matrix (n' i) (p' i) α) :
                                  @[simp]
                                  theorem Matrix.blockDiagonal'RingHom_apply {o : Type u_4} (m' : oType u_7) (α : Type u_12) [DecidableEq o] [(i : o) → DecidableEq (m' i)] [Fintype o] [(i : o) → Fintype (m' i)] [NonAssocSemiring α] (M : (i : o) → Matrix (m' i) (m' i) α) :
                                  def Matrix.blockDiagonal'RingHom {o : Type u_4} (m' : oType u_7) (α : Type u_12) [DecidableEq o] [(i : o) → DecidableEq (m' i)] [Fintype o] [(i : o) → Fintype (m' i)] [NonAssocSemiring α] :
                                  ((i : o) → Matrix (m' i) (m' i) α) →+* Matrix ((i : o) × m' i) ((i : o) × m' i) α

                                  Matrix.blockDiagonal' as a RingHom.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem Matrix.blockDiagonal'_pow {o : Type u_4} {m' : oType u_7} {α : Type u_12} [DecidableEq o] [(i : o) → DecidableEq (m' i)] [Fintype o] [(i : o) → Fintype (m' i)] [Semiring α] (M : (i : o) → Matrix (m' i) (m' i) α) (n : ) :
                                    @[simp]
                                    theorem Matrix.blockDiagonal'_smul {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [DecidableEq o] {R : Type u_14} [Semiring R] [AddCommMonoid α] [Module R α] (x : R) (M : (i : o) → Matrix (m' i) (n' i) α) :
                                    def Matrix.blockDiag' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
                                    Matrix (m' k) (n' k) α

                                    Extract a block from the diagonal of a block diagonal matrix.

                                    This is the block form of Matrix.diag, and the left-inverse of Matrix.blockDiagonal'.

                                    Equations
                                    • M.blockDiag' k = Matrix.of fun (i : m' k) (j : n' k) => M k, i k, j
                                    Instances For
                                      theorem Matrix.blockDiag'_apply {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) (i : m' k) (j : n' k) :
                                      M.blockDiag' k i j = M k, i k, j
                                      theorem Matrix.blockDiag'_map {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} {β : Type u_13} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (f : αβ) :
                                      (M.map f).blockDiag' = fun (k : o) => (M.blockDiag' k).map f
                                      @[simp]
                                      theorem Matrix.blockDiag'_transpose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
                                      M.transpose.blockDiag' k = (M.blockDiag' k).transpose
                                      @[simp]
                                      theorem Matrix.blockDiag'_conjTranspose {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_14} [AddMonoid α] [StarAddMonoid α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
                                      M.conjTranspose.blockDiag' k = (M.blockDiag' k).conjTranspose
                                      @[simp]
                                      theorem Matrix.blockDiag'_zero {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] :
                                      @[simp]
                                      theorem Matrix.blockDiag'_diagonal {o : Type u_4} {m' : oType u_7} {α : Type u_12} [Zero α] [DecidableEq o] [(i : o) → DecidableEq (m' i)] (d : (i : o) × m' iα) (k : o) :
                                      (Matrix.diagonal d).blockDiag' k = Matrix.diagonal fun (i : m' k) => d k, i
                                      @[simp]
                                      theorem Matrix.blockDiag'_blockDiagonal' {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] [DecidableEq o] (M : (i : o) → Matrix (m' i) (n' i) α) :
                                      (Matrix.blockDiagonal' M).blockDiag' = M
                                      theorem Matrix.blockDiagonal'_injective {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] [DecidableEq o] :
                                      Function.Injective Matrix.blockDiagonal'
                                      @[simp]
                                      theorem Matrix.blockDiagonal'_inj {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [Zero α] [DecidableEq o] {M : (i : o) → Matrix (m' i) (n' i) α} {N : (i : o) → Matrix (m' i) (n' i) α} :
                                      @[simp]
                                      theorem Matrix.blockDiag'_one {o : Type u_4} {m' : oType u_7} {α : Type u_12} [Zero α] [DecidableEq o] [(i : o) → DecidableEq (m' i)] [One α] :
                                      @[simp]
                                      theorem Matrix.blockDiag'_add {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [AddZeroClass α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
                                      (M + N).blockDiag' = M.blockDiag' + N.blockDiag'
                                      @[simp]
                                      theorem Matrix.blockDiag'AddMonoidHom_apply {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [AddZeroClass α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (k : o) :
                                      (Matrix.blockDiag'AddMonoidHom m' n' α) M k = M.blockDiag' k
                                      def Matrix.blockDiag'AddMonoidHom {o : Type u_4} (m' : oType u_7) (n' : oType u_8) (α : Type u_12) [AddZeroClass α] :
                                      Matrix ((i : o) × m' i) ((i : o) × n' i) α →+ (i : o) → Matrix (m' i) (n' i) α

                                      Matrix.blockDiag' as an AddMonoidHom.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Matrix.blockDiag'_neg {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [AddGroup α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
                                        (-M).blockDiag' = -M.blockDiag'
                                        @[simp]
                                        theorem Matrix.blockDiag'_sub {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} [AddGroup α] (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (N : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
                                        (M - N).blockDiag' = M.blockDiag' - N.blockDiag'
                                        @[simp]
                                        theorem Matrix.blockDiag'_smul {o : Type u_4} {m' : oType u_7} {n' : oType u_8} {α : Type u_12} {R : Type u_14} [Monoid R] [AddMonoid α] [DistribMulAction R α] (x : R) (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
                                        (x M).blockDiag' = x M.blockDiag'
                                        theorem Matrix.toBlock_mul_eq_mul {R : Type u_10} [CommRing R] {m : Type u_14} {n : Type u_15} {k : Type u_16} [Fintype n] (p : mProp) (q : kProp) (A : Matrix m n R) (B : Matrix n k R) :
                                        (A * B).toBlock p q = A.toBlock p * B.toBlock q
                                        theorem Matrix.toBlock_mul_eq_add {R : Type u_10} [CommRing R] {m : Type u_14} {n : Type u_15} {k : Type u_16} [Fintype n] (p : mProp) (q : nProp) [DecidablePred q] (r : kProp) (A : Matrix m n R) (B : Matrix n k R) :
                                        (A * B).toBlock p r = A.toBlock p q * B.toBlock q r + (A.toBlock p fun (i : n) => ¬q i) * B.toBlock (fun (i : n) => ¬q i) r