Documentation

Mathlib.Data.Matrix.Kronecker

Kronecker product of matrices #

This defines the Kronecker product.

Main definitions #

Specializations #

Notations #

These require open Kronecker:

def Matrix.kroneckerMap {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : αβγ) (A : Matrix l m α) (B : Matrix n p β) :
Matrix (l × n) (m × p) γ

Produce a matrix with f applied to every pair of elements from A and B.

Equations
Instances For
    @[simp]
    theorem Matrix.kroneckerMap_apply {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : αβγ) (A : Matrix l m α) (B : Matrix n p β) (i : l × n) (j : m × p) :
    Matrix.kroneckerMap f A B i j = f (A i.1 j.1) (B i.2 j.2)
    theorem Matrix.kroneckerMap_transpose {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : αβγ) (A : Matrix l m α) (B : Matrix n p β) :
    Matrix.kroneckerMap f A.transpose B.transpose = (Matrix.kroneckerMap f A B).transpose
    theorem Matrix.kroneckerMap_map_left {α : Type u_2} {α' : Type u_3} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α'βγ) (g : αα') (A : Matrix l m α) (B : Matrix n p β) :
    Matrix.kroneckerMap f (A.map g) B = Matrix.kroneckerMap (fun (a : α) (b : β) => f (g a) b) A B
    theorem Matrix.kroneckerMap_map_right {α : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : αβ'γ) (g : ββ') (A : Matrix l m α) (B : Matrix n p β) :
    Matrix.kroneckerMap f A (B.map g) = Matrix.kroneckerMap (fun (a : α) (b : β) => f a (g b)) A B
    theorem Matrix.kroneckerMap_map {α : Type u_2} {β : Type u_4} {γ : Type u_6} {γ' : Type u_7} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : αβγ) (g : γγ') (A : Matrix l m α) (B : Matrix n p β) :
    (Matrix.kroneckerMap f A B).map g = Matrix.kroneckerMap (fun (a : α) (b : β) => g (f a b)) A B
    @[simp]
    theorem Matrix.kroneckerMap_zero_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Zero α] [Zero γ] (f : αβγ) (hf : ∀ (b : β), f 0 b = 0) (B : Matrix n p β) :
    @[simp]
    theorem Matrix.kroneckerMap_zero_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Zero β] [Zero γ] (f : αβγ) (hf : ∀ (a : α), f a 0 = 0) (A : Matrix l m α) :
    theorem Matrix.kroneckerMap_add_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Add α] [Add γ] (f : αβγ) (hf : ∀ (a₁ a₂ : α) (b : β), f (a₁ + a₂) b = f a₁ b + f a₂ b) (A₁ : Matrix l m α) (A₂ : Matrix l m α) (B : Matrix n p β) :
    theorem Matrix.kroneckerMap_add_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Add β] [Add γ] (f : αβγ) (hf : ∀ (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂) (A : Matrix l m α) (B₁ : Matrix n p β) (B₂ : Matrix n p β) :
    theorem Matrix.kroneckerMap_smul_left {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [SMul R α] [SMul R γ] (f : αβγ) (r : R) (hf : ∀ (a : α) (b : β), f (r a) b = r f a b) (A : Matrix l m α) (B : Matrix n p β) :
    theorem Matrix.kroneckerMap_smul_right {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [SMul R β] [SMul R γ] (f : αβγ) (r : R) (hf : ∀ (a : α) (b : β), f a (r b) = r f a b) (A : Matrix l m α) (B : Matrix n p β) :
    theorem Matrix.kroneckerMap_diagonal_diagonal {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [Zero α] [Zero β] [Zero γ] [DecidableEq m] [DecidableEq n] (f : αβγ) (hf₁ : ∀ (b : β), f 0 b = 0) (hf₂ : ∀ (a : α), f a 0 = 0) (a : mα) (b : nβ) :
    Matrix.kroneckerMap f (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun (mn : m × n) => f (a mn.1) (b mn.2)
    theorem Matrix.kroneckerMap_diagonal_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Zero β] [Zero γ] [DecidableEq n] (f : αβγ) (hf : ∀ (a : α), f a 0 = 0) (A : Matrix l m α) (b : nβ) :
    Matrix.kroneckerMap f A (Matrix.diagonal b) = Matrix.blockDiagonal fun (i : n) => A.map fun (a : α) => f a (b i)
    theorem Matrix.kroneckerMap_diagonal_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Zero α] [Zero γ] [DecidableEq l] (f : αβγ) (hf : ∀ (b : β), f 0 b = 0) (a : lα) (B : Matrix m n β) :
    Matrix.kroneckerMap f (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (i : l) => B.map fun (b : β) => f (a i) b)
    @[simp]
    theorem Matrix.kroneckerMap_one_one {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [Zero α] [Zero β] [Zero γ] [One α] [One β] [One γ] [DecidableEq m] [DecidableEq n] (f : αβγ) (hf₁ : ∀ (b : β), f 0 b = 0) (hf₂ : ∀ (a : α), f a 0 = 0) (hf₃ : f 1 1 = 1) :
    theorem Matrix.kroneckerMap_reindex {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} {p' : Type u_17} (f : αβγ) (el : l l') (em : m m') (en : n n') (ep : p p') (M : Matrix l m α) (N : Matrix n p β) :
    Matrix.kroneckerMap f ((Matrix.reindex el em) M) ((Matrix.reindex en ep) N) = (Matrix.reindex (el.prodCongr en) (em.prodCongr ep)) (Matrix.kroneckerMap f M N)
    theorem Matrix.kroneckerMap_reindex_left {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} (f : αβγ) (el : l l') (em : m m') (M : Matrix l m α) (N : Matrix n n' β) :
    Matrix.kroneckerMap f ((Matrix.reindex el em) M) N = (Matrix.reindex (el.prodCongr (Equiv.refl n)) (em.prodCongr (Equiv.refl n'))) (Matrix.kroneckerMap f M N)
    theorem Matrix.kroneckerMap_reindex_right {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} (f : αβγ) (em : m m') (en : n n') (M : Matrix l l' α) (N : Matrix m n β) :
    Matrix.kroneckerMap f M ((Matrix.reindex em en) N) = (Matrix.reindex ((Equiv.refl l).prodCongr em) ((Equiv.refl l').prodCongr en)) (Matrix.kroneckerMap f M N)
    theorem Matrix.kroneckerMap_assoc {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} {δ : Type u_18} {ξ : Type u_19} {ω : Type u_20} {ω' : Type u_21} (f : αβγ) (g : γδω) (f' : αξω') (g' : βδξ) (A : Matrix l m α) (B : Matrix n p β) (D : Matrix q r δ) (φ : ω ω') (hφ : ∀ (a : α) (b : β) (d : δ), φ (g (f a b) d) = f' a (g' b d)) :
    theorem Matrix.kroneckerMap_assoc₁ {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} {δ : Type u_18} {ξ : Type u_19} {ω : Type u_20} (f : αβγ) (g : γδω) (f' : αξω) (g' : βδξ) (A : Matrix l m α) (B : Matrix n p β) (D : Matrix q r δ) (h : ∀ (a : α) (b : β) (d : δ), g (f a b) d = f' a (g' b d)) :
    @[simp]
    theorem Matrix.kroneckerMapBilinear_apply_apply {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (m : Matrix l m✝ α) (B : Matrix n p β) :
    ((Matrix.kroneckerMapBilinear f) m) B = Matrix.kroneckerMap (fun (r : α) (s : β) => (f r) s) m B
    def Matrix.kroneckerMapBilinear {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) :
    Matrix l m α →ₗ[R] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) γ

    When f is bilinear then Matrix.kroneckerMap f is also bilinear.

    Equations
    Instances For
      theorem Matrix.kroneckerMapBilinear_mul_mul {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} [CommSemiring R] [Fintype m] [Fintype m'] [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b') (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) :

      Matrix.kroneckerMapBilinear commutes with * if f does.

      This is primarily used with R = ℕ to prove Matrix.mul_kronecker_mul.

      theorem Matrix.trace_kroneckerMapBilinear {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [CommSemiring R] [Fintype m] [Fintype n] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (A : Matrix m m α) (B : Matrix n n β) :
      (((Matrix.kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace

      trace distributes over Matrix.kroneckerMapBilinear.

      This is primarily used with R = ℕ to prove Matrix.trace_kronecker.

      theorem Matrix.det_kroneckerMapBilinear {R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing α] [CommRing β] [CommRing γ] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b') (A : Matrix m m α) (B : Matrix n n β) :
      (((Matrix.kroneckerMapBilinear f) A) B).det = (A.map fun (a : α) => (f a) 1).det ^ Fintype.card n * (B.map fun (b : β) => (f 1) b).det ^ Fintype.card m

      determinant of Matrix.kroneckerMapBilinear.

      This is primarily used with R = ℕ to prove Matrix.det_kronecker.

      Specialization to Matrix.kroneckerMap (*) #

      def Matrix.kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Mul α] :
      Matrix l m αMatrix n p αMatrix (l × n) (m × p) α

      The Kronecker product. This is just a shorthand for kroneckerMap (*). Prefer the notation ⊗ₖ rather than this definition.

      Equations
      Instances For
        @[simp]
        theorem Matrix.kronecker_apply {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Mul α] (A : Matrix l m α) (B : Matrix n p α) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
        Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ * B i₂ j₂
        def Matrix.kroneckerBilinear {R : Type u_1} {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [Semiring α] [Algebra R α] :
        Matrix l m α →ₗ[R] Matrix n p α →ₗ[R] Matrix (l × n) (m × p) α

        Matrix.kronecker as a bilinear map.

        Equations
        Instances For

          What follows is a copy, in order, of every Matrix.kroneckerMap lemma above that has hypotheses which can be filled by properties of *.

          theorem Matrix.zero_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [MulZeroClass α] (B : Matrix n p α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 0 B = 0
          theorem Matrix.kronecker_zero {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [MulZeroClass α] (A : Matrix l m α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A 0 = 0
          theorem Matrix.add_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Distrib α] (A₁ : Matrix l m α) (A₂ : Matrix l m α) (B : Matrix n p α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (A₁ + A₂) B = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A₁ B + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A₂ B
          theorem Matrix.kronecker_add {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Distrib α] (A : Matrix l m α) (B₁ : Matrix n p α) (B₂ : Matrix n p α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (B₁ + B₂) = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B₁ + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B₂
          theorem Matrix.smul_kronecker {R : Type u_1} {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Monoid R] [Monoid α] [MulAction R α] [IsScalarTower R α α] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (r A) B = r Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B
          theorem Matrix.kronecker_smul {R : Type u_1} {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [Monoid R] [Monoid α] [MulAction R α] [SMulCommClass R α α] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (r B) = r Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B
          theorem Matrix.diagonal_kronecker_diagonal {α : Type u_2} {m : Type u_9} {n : Type u_10} [MulZeroClass α] [DecidableEq m] [DecidableEq n] (a : mα) (b : nα) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.diagonal a) (Matrix.diagonal b) = Matrix.diagonal fun (mn : m × n) => a mn.1 * b mn.2
          theorem Matrix.kronecker_diagonal {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [MulZeroClass α] [DecidableEq n] (A : Matrix l m α) (b : nα) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (Matrix.diagonal b) = Matrix.blockDiagonal fun (i : n) => MulOpposite.op (b i) A
          theorem Matrix.diagonal_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [MulZeroClass α] [DecidableEq l] (a : lα) (B : Matrix m n α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (i : l) => a i B)
          @[simp]
          theorem Matrix.natCast_kronecker_natCast {α : Type u_2} {m : Type u_9} {n : Type u_10} [NonAssocSemiring α] [DecidableEq m] [DecidableEq n] (a : ) (b : ) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) a b = (a * b)
          theorem Matrix.kronecker_natCast {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [NonAssocSemiring α] [DecidableEq n] (A : Matrix l m α) (b : ) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A b = Matrix.blockDiagonal fun (x : n) => b A
          theorem Matrix.natCast_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [NonAssocSemiring α] [DecidableEq l] (a : ) (B : Matrix m n α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (↑a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (x : l) => a B)
          theorem Matrix.kronecker_ofNat {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Semiring α] [DecidableEq n] (A : Matrix l m α) (b : ) [b.AtLeastTwo] :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (OfNat.ofNat b) = Matrix.blockDiagonal fun (x : n) => MulOpposite.op (OfNat.ofNat b) A
          theorem Matrix.ofNat_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Semiring α] [DecidableEq l] (a : ) [a.AtLeastTwo] (B : Matrix m n α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (OfNat.ofNat a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (x : l) => OfNat.ofNat a B)
          theorem Matrix.one_kronecker_one {α : Type u_2} {m : Type u_9} {n : Type u_10} [MulZeroOneClass α] [DecidableEq m] [DecidableEq n] :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 1 1 = 1
          theorem Matrix.kronecker_one {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [MulZeroOneClass α] [DecidableEq n] (A : Matrix l m α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A 1 = Matrix.blockDiagonal fun (x : n) => A
          theorem Matrix.one_kronecker {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [MulZeroOneClass α] [DecidableEq l] (B : Matrix m n α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) 1 B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun (x : l) => B)
          theorem Matrix.mul_kronecker_mul {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} [Fintype m] [Fintype m'] [CommSemiring α] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' α) (B' : Matrix m' n' α) :
          Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (A * B) (A' * B') = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A A' * Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) B B'
          theorem Matrix.kronecker_assoc {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
          (Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B) C) = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) B C)
          @[simp]
          theorem Matrix.kronecker_assoc' {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [Semigroup α] (A : Matrix l m α) (B : Matrix n p α) (C : Matrix q r α) :
          (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B) C).submatrix (Equiv.prodAssoc l n q).symm (Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) B C)
          theorem Matrix.trace_kronecker {α : Type u_2} {m : Type u_9} {n : Type u_10} [Fintype m] [Fintype n] [Semiring α] (A : Matrix m m α) (B : Matrix n n α) :
          (Matrix.kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B).trace = A.trace * B.trace
          theorem Matrix.det_kronecker {R : Type u_1} {m : Type u_9} {n : Type u_10} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] (A : Matrix m m R) (B : Matrix n n R) :
          (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m
          theorem Matrix.inv_kronecker {R : Type u_1} {m : Type u_9} {n : Type u_10} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [CommRing R] (A : Matrix m m R) (B : Matrix n n R) :
          (Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B)⁻¹ = Matrix.kroneckerMap (fun (x1 x2 : R) => x1 * x2) A⁻¹ B⁻¹

          Specialization to Matrix.kroneckerMap (⊗ₜ) #

          noncomputable def Matrix.kroneckerTMul (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] :
          Matrix l m αMatrix n p βMatrix (l × n) (m × p) (TensorProduct R α β)

          The Kronecker tensor product. This is just a shorthand for kroneckerMap (⊗ₜ). Prefer the notation ⊗ₖₜ rather than this definition.

          Equations
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Matrix.kroneckerTMul_apply (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (A : Matrix l m α) (B : Matrix n p β) (i₁ : l) (i₂ : n) (j₁ : m) (j₂ : p) :
              Matrix.kroneckerMap (fun (x1 : α) (x2 : β) => x1 ⊗ₜ[R] x2) A B (i₁, i₂) (j₁, j₂) = A i₁ j₁ ⊗ₜ[R] B i₂ j₂
              noncomputable def Matrix.kroneckerTMulBilinear (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] :
              Matrix l m α →ₗ[R] Matrix n p β →ₗ[R] Matrix (l × n) (m × p) (TensorProduct R α β)

              Matrix.kronecker as a bilinear map.

              Equations
              Instances For

                What follows is a copy, in order, of every Matrix.kroneckerMap lemma above that has hypotheses which can be filled by properties of ⊗ₜ.

                theorem Matrix.zero_kroneckerTMul (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (B : Matrix n p β) :
                theorem Matrix.kroneckerTMul_zero (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (A : Matrix l m α) :
                theorem Matrix.add_kroneckerTMul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [Module R α] (A₁ : Matrix l m α) (A₂ : Matrix l m α) (B : Matrix n p α) :
                Matrix.kroneckerMap (TensorProduct.tmul R) (A₁ + A₂) B = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A₁ B + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A₂ B
                theorem Matrix.kroneckerTMul_add (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [Module R α] (A : Matrix l m α) (B₁ : Matrix n p α) (B₂ : Matrix n p α) :
                Matrix.kroneckerMap (TensorProduct.tmul R) A (B₁ + B₂) = Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B₁ + Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B₂
                theorem Matrix.smul_kroneckerTMul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [Module R α] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
                Matrix.kroneckerMap (TensorProduct.tmul R) (r A) B = r Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B
                theorem Matrix.kroneckerTMul_smul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} [CommSemiring R] [AddCommMonoid α] [Module R α] (r : R) (A : Matrix l m α) (B : Matrix n p α) :
                Matrix.kroneckerMap (TensorProduct.tmul R) A (r B) = r Matrix.kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A B
                theorem Matrix.diagonal_kroneckerTMul_diagonal (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [CommSemiring R] [AddCommMonoid α] [Module R α] [DecidableEq m] [DecidableEq n] (a : mα) (b : nα) :
                theorem Matrix.kroneckerTMul_diagonal (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [CommSemiring R] [AddCommMonoid α] [Module R α] [DecidableEq n] (A : Matrix l m α) (b : nα) :
                Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.diagonal b) = Matrix.blockDiagonal fun (i : n) => A.map fun (a : α) => a ⊗ₜ[R] b i
                theorem Matrix.diagonal_kroneckerTMul (R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [CommSemiring R] [AddCommMonoid α] [Module R α] [DecidableEq l] (a : lα) (B : Matrix m n α) :
                theorem Matrix.kroneckerTMul_assoc (R : Type u_1) {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
                @[simp]
                theorem Matrix.kroneckerTMul_assoc' (R : Type u_1) {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) :
                theorem Matrix.trace_kroneckerTMul (R : Type u_1) {α : Type u_2} {β : Type u_4} {m : Type u_9} {n : Type u_10} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] [Fintype m] [Fintype n] (A : Matrix m m α) (B : Matrix n n β) :
                (Matrix.kroneckerMap (TensorProduct.tmul R) A B).trace = A.trace ⊗ₜ[R] B.trace
                @[simp]
                theorem Matrix.one_kroneckerTMul_one (R : Type u_1) {α : Type u_2} {m : Type u_9} {n : Type u_10} [CommSemiring R] [Semiring α] [Algebra R α] [DecidableEq m] [DecidableEq n] :
                theorem Matrix.mul_kroneckerTMul_mul (R : Type u_1) {α : Type u_2} {β : Type u_4} {l : Type u_8} {m : Type u_9} {n : Type u_10} {l' : Type u_14} {m' : Type u_15} {n' : Type u_16} [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] [Fintype m] [Fintype m'] (A : Matrix l m α) (B : Matrix m n α) (A' : Matrix l' m' β) (B' : Matrix m' n' β) :
                theorem Matrix.det_kroneckerTMul (R : Type u_1) {α : Type u_2} {β : Type u_4} {m : Type u_9} {n : Type u_10} [CommRing R] [CommRing α] [CommRing β] [Algebra R α] [Algebra R β] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m m α) (B : Matrix n n β) :