Documentation

Monlib.LinearAlgebra.Matrix.IncludeBlock

Include block #

This file defines matrix.includeBlock which immitates direct_sum.component_of but for pi instead of direct_sum :TODO:

The direct sum in these files are sort of misleading.

theorem Finset.sum_sigma_univ {β : Type u_1} {α : Type u_2} [AddCommMonoid β] [Fintype α] {σ : αType u_3} [(i : α) → Fintype (σ i)] (f : (i : α) × σ iβ) :
x : (i : α) × σ i, f x = a : α, s : σ a, f a, s
def Matrix.blockDiagonal'AlgHom {o : Type u_1} {m' : oType u_2} {α : Type u_3} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] :
PiMat α o m' →ₐ[α] Matrix ((i : o) × m' i) ((i : o) × m' i) α
Equations
Instances For
    theorem Matrix.blockDiagonal'AlgHom_apply {o : Type u_1} {m' : oType u_2} {α : Type u_3} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] (x : PiMat α o m') :
    def Matrix.blockDiag'LinearMap {o : Type u_1} {m' : oType u_2} {n' : oType u_3} {α : Type u_4} [Semiring α] :
    Matrix ((i : o) × m' i) ((i : o) × n' i) α →ₗ[α] (i : o) → Matrix (m' i) (n' i) α
    Equations
    Instances For
      theorem Matrix.blockDiag'LinearMap_apply {o : Type u_1} {m' : oType u_2} {n' : oType u_3} {α : Type u_4} [Semiring α] (x : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
      theorem Matrix.blockDiag'LinearMap_blockDiagonal'AlgHom {o : Type u_1} {m' : oType u_2} {α : Type u_3} [Fintype o] [DecidableEq o] [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] (x : PiMat α o m') :
      theorem Matrix.blockDiagonal'_ext {R : Type u_1} {k : Type u_2} {s : kType u_3} (x y : Matrix ((i : k) × s i) ((i : k) × s i) R) :
      x = y ∀ (i : k) (j : s i) (k_1 : k) (l : s k_1), x i, j k_1, l = y i, j k_1, l
      def Matrix.IsBlockDiagonal {o : Type u_1} {m' : oType u_2} {n' : oType u_3} {α : Type u_4} [DecidableEq o] [Zero α] (x : Matrix ((i : o) × m' i) ((i : o) × n' i) α) :
      Equations
      Instances For
        def Matrix.includeBlock {o : Type u_1} [DecidableEq o] {m' : oType u_2} {α : Type u_3} [Semiring α] {i : o} :
        Matrix (m' i) (m' i) α →ₗ[α] PiMat α o m'
        Equations
        Instances For
          theorem Matrix.includeBlock_apply {o : Type u_1} [DecidableEq o] {m' : oType u_2} {α : Type u_3} [CommSemiring α] {i : o} (x : Matrix (m' i) (m' i) α) :
          includeBlock x = fun (j : o) => if h : i = j then .mp x else 0
          theorem Matrix.includeBlock_hMul_same {o : Type u_1} [Fintype o] [DecidableEq o] {m' : oType u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] {i : o} (x y : Matrix (m' i) (m' i) α) :
          theorem Matrix.includeBlock_hMul_ne_same {o : Type u_1} [Fintype o] [DecidableEq o] {m' : oType u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] {i j : o} (h : i j) (x : Matrix (m' i) (m' i) α) (y : Matrix (m' j) (m' j) α) :
          theorem Matrix.includeBlock_hMul {o : Type u_1} [Fintype o] [DecidableEq o] {m' : oType u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] {i : o} (x : Matrix (m' i) (m' i) α) (y : PiMat α o m') :
          theorem Matrix.hMul_includeBlock {o : Type u_1} [Fintype o] [DecidableEq o] {m' : oType u_2} {α : Type u_3} [(i : o) → Fintype (m' i)] [(i : o) → DecidableEq (m' i)] [CommSemiring α] {i : o} (x : PiMat α o m') (y : Matrix (m' i) (m' i) α) :
          theorem Matrix.sum_includeBlock {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : PiMat R k s) :
          i : k, includeBlock (x i) = x
          theorem Matrix.blockDiagonal'_includeBlock_trace {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : PiMat R k s) (j : k) :
          theorem Matrix.stdBasisMatrix_hMul_trace {R : Type u_1} {n : Type u_2} {p : Type u_3} [Semiring R] [Fintype p] [DecidableEq p] [Fintype n] [DecidableEq n] (i : n) (j : p) (x : Matrix p n R) :
          (stdBasisMatrix i j 1 * x).trace = x j i
          theorem Matrix.ext_iff_trace {R : Type u_1} {n : Type u_2} {p : Type u_3} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p] [CommSemiring R] (x y : Matrix n p R) :
          x = y ∀ (a : Matrix p n R), (x * a).trace = (y * a).trace
          theorem Matrix.IsBlockDiagonal.eq {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : kType u_2} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) :
          theorem Matrix.IsBlockDiagonal.add {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : kType u_2} {x y : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (hy : y.IsBlockDiagonal) :
          @[reducible]
          def Matrix.BlockDiagonals (R : Type u_1) (k : Type u_2) [Zero R] [DecidableEq k] (s : kType u_3) :
          Type (max 0 (max u_1 u_2) u_3)
          Equations
          Instances For
            theorem Matrix.IsBlockDiagonal.zero {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : kType u_2} :
            instance Matrix.IsBlockDiagonal.HAdd {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : kType u_3} :
            Equations
            theorem Matrix.IsBlockDiagonal.coe_add {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {x y : BlockDiagonals R k s} :
            ↑(x + y) = x + y
            instance Matrix.IsBlockDiagonal.Zero {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
            Equations
            theorem Matrix.IsBlockDiagonal.coe_zero {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
            0 = 0
            theorem Matrix.IsBlockDiagonal.smul {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : kType u_2} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (α : R) :
            instance Matrix.IsBlockDiagonal.Smul {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
            Equations
            theorem Matrix.IsBlockDiagonal.coe_smul {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (a : R) (x : BlockDiagonals R k s) :
            ↑(a x) = a x
            instance Matrix.addCommMonoidBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
            Equations
            theorem Matrix.IsBlockDiagonal.coe_sum {R : Type u_4} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {n : Type u_3} [Fintype n] {x : nBlockDiagonals R k s} :
            (∑ i : n, x i) = i : n, (x i)
            instance Matrix.mulActionBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
            Equations
            instance Matrix.distribMulActionBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
            Equations
            instance Matrix.moduleBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
            Equations
            theorem Matrix.isBlockDiagonal_iff {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : kType u_2} (x : Matrix ((i : k) × s i) ((i : k) × s i) R) :
            x.IsBlockDiagonal ∃ (y : PiMat R k s), x = blockDiagonal' y
            def Matrix.stdBasisMatrixBlockDiagonal {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : kType u_3} [(i : k) → DecidableEq (s i)] (i : k) (j l : s i) (α : R) :
            Equations
            Instances For
              theorem Matrix.includeBlock_conjTranspose {R : Type u_1} {k : Type u_2} [CommSemiring R] [StarRing R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i : k} {x : Matrix (s i) (s i) R} :
              theorem Matrix.includeBlock_inj {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i : k} {x y : Matrix (s i) (s i) R} :
              theorem Matrix.blockDiagonal'_includeBlock_isHermitian_iff {R : Type u_1} {k : Type u_2} [CommSemiring R] [StarRing R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i : k} (x : Matrix (s i) (s i) R) :
              theorem Matrix.matrix_eq_sum_includeBlock {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : PiMat R k s) :
              x = i : k, includeBlock (x i)
              theorem Matrix.includeBlock_apply_same {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i : k} (x : Matrix (s i) (s i) R) :
              theorem Matrix.includeBlock_apply_ne_same {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i j : k} (x : Matrix (s i) (s i) R) (h : i j) :
              theorem Matrix.includeBlock_apply_stdBasisMatrix {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i : k} (a b : s i) :
              includeBlock (stdBasisMatrix a b 1) = (stdBasisMatrix i, a i, b 1).blockDiag'
              theorem Matrix.includeBlock_hMul_includeBlock {R : Type u_1} {k : Type u_2} [CommSemiring R] [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {i j : k} (x : Matrix (s i) (s i) R) (y : Matrix (s j) (s j) R) :
              includeBlock x * includeBlock y = if h : j = i then includeBlock (x * .mpr y) else 0
              theorem Matrix.IsBlockDiagonal.mul {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] {x y : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (hy : y.IsBlockDiagonal) :
              instance Matrix.IsBlockDiagonal.hasMul {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
              Equations
              theorem Matrix.IsBlockDiagonal.coe_mul {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {x y : BlockDiagonals R k s} :
              ↑(x * y) = x * y
              theorem Matrix.IsBlockDiagonal.one {R : Type u_3} [CommSemiring R] {k : Type u_1} [DecidableEq k] {s : kType u_2} [(i : k) → DecidableEq (s i)] :
              instance Matrix.IsBlockDiagonal.hasOne {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : kType u_3} [(i : k) → DecidableEq (s i)] :
              Equations
              theorem Matrix.IsBlockDiagonal.coe_one {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
              1 = 1
              theorem Matrix.IsBlockDiagonal.coe_nsmul {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (n : ) (x : BlockDiagonals R k s) :
              ↑(n x) = n x
              theorem Matrix.IsBlockDiagonal.npow {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (n : ) {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) :
              instance Matrix.IsBlockDiagonal.hasNpow {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
              Equations
              theorem Matrix.IsBlockDiagonal.coe_npow {R : Type u_3} [CommSemiring R] {k : Type u_1} [Fintype k] [DecidableEq k] {s : kType u_2} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (n : ) (x : BlockDiagonals R k s) :
              ↑(x ^ n) = x ^ n
              instance Matrix.IsBlockDiagonal.semiring {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
              Equations
              instance Matrix.IsBlockDiagonal.algebra {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
              Equations
              def Matrix.isBlockDiagonalPiAlgEquiv {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem Matrix.isBlockDiagonalPiAlgEquiv_symm_apply_coe {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : PiMat R k s) :
                @[simp]
                theorem Matrix.isBlockDiagonalPiAlgEquiv_apply {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : BlockDiagonals R k s) (k✝ : k) :
                theorem Matrix.IsBlockDiagonal.star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [DecidableEq k] {s : kType u_3} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) :
                instance Matrix.IsBlockDiagonal.hasStar {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] :
                Equations
                theorem Matrix.IsBlockDiagonal.coe_star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (y : BlockDiagonals R k s) :
                (Star.star y) = (↑y).conjTranspose
                theorem Matrix.isBlockDiagonalPiAlgEquiv.map_star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : BlockDiagonals R k s) :
                theorem Matrix.isBlockDiagonalPiAlgEquiv.symm_map_star {R : Type u_1} [CommSemiring R] [StarAddMonoid R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : PiMat R k s) :
                def Matrix.Equiv.sigmaProdDistrib' {ι : Type u_1} (β : Type u_2) (α : ιType u_3) :
                β × (i : ι) × α i (i : ι) × β × α i
                Equations
                Instances For
                  @[simp]
                  theorem Matrix.Equiv.sigmaProdDistrib'_apply_fst {ι : Type u_1} (β : Type u_2) (α : ιType u_3) (a✝ : β × (i : ι) × α i) :
                  ((sigmaProdDistrib' β α) a✝).fst = a✝.2.fst
                  @[simp]
                  theorem Matrix.Equiv.sigmaProdDistrib'_apply_snd {ι : Type u_1} (β : Type u_2) (α : ιType u_3) (a✝ : β × (i : ι) × α i) :
                  ((sigmaProdDistrib' β α) a✝).snd = (a✝.1, a✝.2.snd)
                  @[simp]
                  theorem Matrix.Equiv.sigmaProdDistrib'_symm_apply {ι : Type u_1} (β : Type u_2) (α : ιType u_3) (a✝ : (i : ι) × β × α i) :
                  (sigmaProdDistrib' β α).symm a✝ = (a✝.snd.1, a✝.fst, a✝.snd.2)
                  def Matrix.sigmaProdSigma {α : Type u_1} {β : Type u_2} {ζ : αType u_3} { : βType u_4} :
                  ((i : α) × ζ i) × (i : β) × i (i : α) × (j : β) × ζ i × j
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Matrix.sigmaProdSigma_apply_snd_fst {α : Type u_1} {β : Type u_2} {ζ : αType u_3} { : βType u_4} (x : ((i : α) × ζ i) × (i : β) × i) :
                    (sigmaProdSigma x).snd.fst = ((Equiv.sigmaProdDistrib' ((i : α) × ζ i) ) x).fst
                    @[simp]
                    theorem Matrix.sigmaProdSigma_apply_fst {α : Type u_1} {β : Type u_2} {ζ : αType u_3} { : βType u_4} (x : ((i : α) × ζ i) × (i : β) × i) :
                    (sigmaProdSigma x).fst = ((Equiv.sigmaProdDistrib ζ ((i : β) × i)) x).fst
                    @[simp]
                    theorem Matrix.sigmaProdSigma_apply_snd_snd {α : Type u_1} {β : Type u_2} {ζ : αType u_3} { : βType u_4} (x : ((i : α) × ζ i) × (i : β) × i) :
                    @[simp]
                    theorem Matrix.sigmaProdSigma_symm_apply {α : Type u_1} {β : Type u_2} {ζ : αType u_3} { : βType u_4} (x : (i : α) × (j : β) × ζ i × j) :
                    sigmaProdSigma.symm x = (x.fst, x.snd.snd.1, x.snd.fst, x.snd.snd.2)
                    theorem Matrix.IsBlockDiagonal.apply_of_ne {R : Type u_1} [CommSemiring R] {k : Type u_2} [DecidableEq k] {s : kType u_3} {x : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) (i j : (i : k) × s i) (h : i.fst j.fst) :
                    x i j = 0
                    theorem Matrix.IsBlockDiagonal.apply_of_ne_coe {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (x : BlockDiagonals R k s) (i j : (i : k) × s i) (h : i.fst j.fst) :
                    x i j = 0
                    theorem Matrix.IsBlockDiagonal.kronecker_hMul {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] {x y : Matrix ((i : k) × s i) ((i : k) × s i) R} (hx : x.IsBlockDiagonal) :
                    IsBlockDiagonal fun (i j : (i : k) × (j : k) × s i × s j) => kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y (sigmaProdSigma.symm i) (sigmaProdSigma.symm j)
                    @[simp]
                    theorem Matrix.directSumLinearMapAlgEquivIsBlockDiagonalLinearMap_apply_apply_coe {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (a : Module.End R (PiMat R k s)) (a✝ : BlockDiagonals R k s) :
                    @[simp]
                    theorem Matrix.directSumLinearMapAlgEquivIsBlockDiagonalLinearMap_symm_apply_apply {R : Type u_1} [CommSemiring R] {k : Type u_2} [Fintype k] [DecidableEq k] {s : kType u_3} [(i : k) → Fintype (s i)] [(i : k) → DecidableEq (s i)] (a : Module.End R (BlockDiagonals R k s)) (a✝ : PiMat R k s) (i : k) :