Kronecker product of matrices #
This defines the Kronecker product.
Main definitions #
Matrix.kroneckerMap: A generalization of the Kronecker product: given a mapf : α → β → γand matricesAandBwith coefficients inαandβ, respectively, it is defined as the matrix with coefficients inγsuch thatkroneckerMap f A B (i₁, i₂) (j₁, j₂) = f (A i₁ j₁) (B i₁ j₂).Matrix.kroneckerMapBilinear: whenfis bilinear, so iskroneckerMap f.
Specializations #
Matrix.kronecker: An alias ofkroneckerMap (*). Prefer using the notation.Matrix.kroneckerBilinear:Matrix.kroneckeris bilinearMatrix.kroneckerTMul: An alias ofkroneckerMap (⊗ₜ). Prefer using the notation.Matrix.kroneckerTMulBilinear:Matrix.kroneckerTMulis bilinear
Notation #
These require open Kronecker:
A ⊗ₖ BforkroneckerMap (*) A B. Lemmas about this notation use the tokenkronecker.A ⊗ₖₜ BandA ⊗ₖₜ[R] BforkroneckerMap (⊗ₜ) A B. Lemmas about this notation use the tokenkroneckerTMul.
def
Matrix.kroneckerMap
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
(f : α → β → γ)
(A : Matrix l m α)
(B : Matrix n p β)
:
Produce a matrix with f applied to every pair of elements from A and B.
Equations
- Matrix.kroneckerMap f A B = Matrix.of fun (i : l × n) (j : m × p) => f (A i.1 j.1) (B i.2 j.2)
Instances For
theorem
Matrix.kroneckerMap_single_single
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Zero α]
[Zero β]
[Zero γ]
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[DecidableEq p]
(i₁ : l)
(j₁ : m)
(i₂ : n)
(j₂ : p)
(f : α → β → γ)
(hf₁ : ∀ (b : β), f 0 b = 0)
(hf₂ : ∀ (a : α), f a 0 = 0)
(a : α)
(b : β)
:
@[deprecated Matrix.kroneckerMap_single_single (since := "2025-05-05")]
theorem
Matrix.kroneckerMap_stdBasisMatrix_stdBasisMatrix
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Zero α]
[Zero β]
[Zero γ]
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[DecidableEq p]
(i₁ : l)
(j₁ : m)
(i₂ : n)
(j₂ : p)
(f : α → β → γ)
(hf₁ : ∀ (b : β), f 0 b = 0)
(hf₂ : ∀ (a : α), f a 0 = 0)
(a : α)
(b : β)
:
Alias of Matrix.kroneckerMap_single_single.
theorem
Matrix.kroneckerMap_diagonal_diagonal
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{m : Type u_10}
{n : Type u_11}
[Zero α]
[Zero β]
[Zero γ]
[DecidableEq m]
[DecidableEq n]
(f : α → β → γ)
(hf₁ : ∀ (b : β), f 0 b = 0)
(hf₂ : ∀ (a : α), f a 0 = 0)
(a : m → α)
(b : n → β)
:
theorem
Matrix.kroneckerMap_diagonal_left
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[Zero α]
[Zero γ]
[DecidableEq l]
(f : α → β → γ)
(hf : ∀ (b : β), f 0 b = 0)
(a : l → α)
(B : Matrix m n β)
:
kroneckerMap f (diagonal a) B = (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun (i : l) => B.map fun (b : β) => f (a i) b)
theorem
Matrix.kroneckerMap_reindex
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
{l' : Type u_15}
{m' : Type u_16}
{n' : Type u_17}
{p' : Type u_18}
(f : α → β → γ)
(el : l ≃ l')
(em : m ≃ m')
(en : n ≃ n')
(ep : p ≃ p')
(M : Matrix l m α)
(N : Matrix n p β)
:
kroneckerMap f ((reindex el em) M) ((reindex en ep) N) = (reindex (el.prodCongr en) (em.prodCongr ep)) (kroneckerMap f M N)
theorem
Matrix.kroneckerMap_reindex_left
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{l' : Type u_15}
{m' : Type u_16}
{n' : Type u_17}
(f : α → β → γ)
(el : l ≃ l')
(em : m ≃ m')
(M : Matrix l m α)
(N : Matrix n n' β)
:
kroneckerMap f ((reindex el em) M) N = (reindex (el.prodCongr (Equiv.refl n)) (em.prodCongr (Equiv.refl n'))) (kroneckerMap f M N)
theorem
Matrix.kroneckerMap_reindex_right
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{l' : Type u_15}
{m' : Type u_16}
{n' : Type u_17}
(f : α → β → γ)
(em : m ≃ m')
(en : n ≃ n')
(M : Matrix l l' α)
(N : Matrix m n β)
:
kroneckerMap f M ((reindex em en) N) = (reindex ((Equiv.refl l).prodCongr em) ((Equiv.refl l').prodCongr en)) (kroneckerMap f M N)
theorem
Matrix.kroneckerMap_assoc
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
{q : Type u_13}
{r : Type u_14}
{δ : Type u_19}
{ξ : Type u_20}
{ω : Type u_21}
{ω' : Type u_22}
(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))
:
((reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)).trans φ.mapMatrix) (kroneckerMap g (kroneckerMap f A B) D) = kroneckerMap f' A (kroneckerMap g' B D)
theorem
Matrix.kroneckerMap_assoc₁
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
{q : Type u_13}
{r : Type u_14}
{δ : 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))
:
(reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) (kroneckerMap g (kroneckerMap f A B) D) = kroneckerMap f' A (kroneckerMap g' B D)
def
Matrix.kroneckerMapBilinear
{R : Type u_1}
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Semiring S]
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R γ]
[Module S β]
[Module S γ]
[SMulCommClass S R γ]
(f : α →ₗ[R] β →ₗ[S] γ)
:
When f is bilinear then Matrix.kroneckerMap f is also bilinear.
Equations
- Matrix.kroneckerMapBilinear f = LinearMap.mk₂' R S (Matrix.kroneckerMap fun (r : α) (s : β) => (f r) s) ⋯ ⋯ ⋯ ⋯
Instances For
@[simp]
theorem
Matrix.kroneckerMapBilinear_apply_apply
{R : Type u_1}
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Semiring S]
[Semiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R γ]
[Module S β]
[Module S γ]
[SMulCommClass S R γ]
(f : α →ₗ[R] β →ₗ[S] γ)
(m✝ : Matrix l m α)
(B : Matrix n p β)
:
theorem
Matrix.kroneckerMapBilinear_mul_mul
{R : Type u_1}
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{l' : Type u_15}
{m' : Type u_16}
{n' : Type u_17}
[Semiring S]
[Semiring R]
[Fintype m]
[Fintype m']
[NonUnitalNonAssocSemiring α]
[NonUnitalNonAssocSemiring β]
[NonUnitalNonAssocSemiring γ]
[Module R α]
[Module R γ]
[Module S β]
[Module S γ]
[SMulCommClass S R γ]
(f : α →ₗ[R] β →ₗ[S] γ)
(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' β)
:
((kroneckerMapBilinear f) (A * B)) (A' * B') = ((kroneckerMapBilinear f) A) A' * ((kroneckerMapBilinear f) B) B'
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}
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{m : Type u_10}
{n : Type u_11}
[Semiring S]
[Semiring R]
[Fintype m]
[Fintype n]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R γ]
[Module S β]
[Module S γ]
[SMulCommClass S R γ]
(f : α →ₗ[R] β →ₗ[S] γ)
(A : Matrix m m α)
(B : Matrix n n β)
:
trace distributes over Matrix.kroneckerMapBilinear.
This is primarily used with R = ℕ to prove Matrix.trace_kronecker.
theorem
Matrix.det_kroneckerMapBilinear
{R : Type u_1}
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{m : Type u_10}
{n : Type u_11}
[Semiring S]
[Semiring R]
[Fintype m]
[Fintype n]
[DecidableEq m]
[DecidableEq n]
[NonAssocSemiring α]
[NonAssocSemiring β]
[CommRing γ]
[Module R α]
[Module S β]
[Module R γ]
[Module S γ]
[SMulCommClass S R γ]
(f : α →ₗ[R] β →ₗ[S] γ)
(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 β)
:
(((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_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Mul α]
:
The Kronecker product. This is just a shorthand for kroneckerMap (*). Prefer the notation
⊗ₖ rather than this definition.
Equations
- Matrix.kronecker = Matrix.kroneckerMap fun (x1 x2 : α) => x1 * x2
Instances For
Produce a matrix with f applied to every pair of elements from A and B.
Equations
- Kronecker.«term_⊗ₖ_» = Lean.ParserDescr.trailingNode `Kronecker.«term_⊗ₖ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₖ ") (Lean.ParserDescr.cat `term 101))
Instances For
def
Matrix.kroneckerBilinear
{R : Type u_1}
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[Semiring α]
[Algebra 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_kronecker
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[MulZeroClass α]
(B : Matrix n p α)
:
theorem
Matrix.kronecker_zero
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[MulZeroClass α]
(A : Matrix l m α)
:
theorem
Matrix.add_kronecker
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Distrib α]
(A₁ A₂ : Matrix l m α)
(B : Matrix n p α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) (A₁ + A₂) B = kroneckerMap (fun (x1 x2 : α) => x1 * x2) A₁ B + kroneckerMap (fun (x1 x2 : α) => x1 * x2) A₂ B
theorem
Matrix.kronecker_add
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Distrib α]
(A : Matrix l m α)
(B₁ B₂ : Matrix n p α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (B₁ + B₂) = kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B₁ + kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B₂
theorem
Matrix.smul_kronecker
{R : Type u_1}
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Mul α]
[SMul R α]
[IsScalarTower R α α]
(r : R)
(A : Matrix l m α)
(B : Matrix n p α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) (r • A) B = r • kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B
theorem
Matrix.kronecker_smul
{R : Type u_1}
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Mul α]
[SMul R α]
[SMulCommClass R α α]
(r : R)
(A : Matrix l m α)
(B : Matrix n p α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (r • B) = r • kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B
theorem
Matrix.single_kronecker_single
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[MulZeroClass α]
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[DecidableEq p]
(ia : l)
(ja : m)
(ib : n)
(jb : p)
(a b : α)
:
@[deprecated Matrix.single_kronecker_single (since := "2025-05-05")]
theorem
Matrix.stdBasisMatrix_kronecker_stdBasisMatrix
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[MulZeroClass α]
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[DecidableEq p]
(ia : l)
(ja : m)
(ib : n)
(jb : p)
(a b : α)
:
Alias of Matrix.single_kronecker_single.
theorem
Matrix.diagonal_kronecker_diagonal
{α : Type u_3}
{m : Type u_10}
{n : Type u_11}
[MulZeroClass α]
[DecidableEq m]
[DecidableEq n]
(a : m → α)
(b : n → α)
:
theorem
Matrix.kronecker_diagonal
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[MulZeroClass α]
[DecidableEq n]
(A : Matrix l m α)
(b : n → α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (diagonal b) = blockDiagonal fun (i : n) => MulOpposite.op (b i) • A
theorem
Matrix.diagonal_kronecker
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[MulZeroClass α]
[DecidableEq l]
(a : l → α)
(B : Matrix m n α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) (diagonal a) B = (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun (i : l) => a i • B)
@[simp]
theorem
Matrix.natCast_kronecker_natCast
{α : Type u_3}
{m : Type u_10}
{n : Type u_11}
[NonAssocSemiring α]
[DecidableEq m]
[DecidableEq n]
(a b : ℕ)
:
theorem
Matrix.kronecker_natCast
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[NonAssocSemiring α]
[DecidableEq n]
(A : Matrix l m α)
(b : ℕ)
:
theorem
Matrix.natCast_kronecker
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[NonAssocSemiring α]
[DecidableEq l]
(a : ℕ)
(B : Matrix m n α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) (↑a) B = (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun (x : l) => a • B)
theorem
Matrix.kronecker_ofNat
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[NonAssocSemiring α]
[DecidableEq n]
(A : Matrix l m α)
(b : ℕ)
[b.AtLeastTwo]
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (OfNat.ofNat b) = blockDiagonal fun (x : n) => MulOpposite.op (OfNat.ofNat b) • A
theorem
Matrix.ofNat_kronecker
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[NonAssocSemiring α]
[DecidableEq l]
(a : ℕ)
[a.AtLeastTwo]
(B : Matrix m n α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) (OfNat.ofNat a) B = (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun (x : l) => OfNat.ofNat a • B)
theorem
Matrix.one_kronecker_one
{α : Type u_3}
{m : Type u_10}
{n : Type u_11}
[MulZeroOneClass α]
[DecidableEq m]
[DecidableEq n]
:
theorem
Matrix.kronecker_one
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[MulZeroOneClass α]
[DecidableEq n]
(A : Matrix l m α)
:
theorem
Matrix.one_kronecker
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[MulZeroOneClass α]
[DecidableEq l]
(B : Matrix m n α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) 1 B = (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun (x : l) => B)
theorem
Matrix.mul_kronecker_mul
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{l' : Type u_15}
{m' : Type u_16}
{n' : Type u_17}
[Fintype m]
[Fintype m']
[CommSemiring α]
(A : Matrix l m α)
(B : Matrix m n α)
(A' : Matrix l' m' α)
(B' : Matrix m' n' α)
:
kroneckerMap (fun (x1 x2 : α) => x1 * x2) (A * B) (A' * B') = kroneckerMap (fun (x1 x2 : α) => x1 * x2) A A' * kroneckerMap (fun (x1 x2 : α) => x1 * x2) B B'
theorem
Matrix.kronecker_assoc
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
{q : Type u_13}
{r : Type u_14}
[Semigroup α]
(A : Matrix l m α)
(B : Matrix n p α)
(C : Matrix q r α)
:
(reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r))
(kroneckerMap (fun (x1 x2 : α) => x1 * x2) (kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B) C) = kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (kroneckerMap (fun (x1 x2 : α) => x1 * x2) B C)
@[simp]
theorem
Matrix.kronecker_assoc'
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
{q : Type u_13}
{r : Type u_14}
[Semigroup α]
(A : Matrix l m α)
(B : Matrix n p α)
(C : Matrix q r α)
:
(kroneckerMap (fun (x1 x2 : α) => x1 * x2) (kroneckerMap (fun (x1 x2 : α) => x1 * x2) A B) C).submatrix
⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = kroneckerMap (fun (x1 x2 : α) => x1 * x2) A (kroneckerMap (fun (x1 x2 : α) => x1 * x2) B C)
theorem
Matrix.det_kronecker
{R : Type u_1}
{m : Type u_10}
{n : Type u_11}
[Fintype m]
[Fintype n]
[DecidableEq m]
[DecidableEq n]
[CommRing R]
(A : Matrix m m R)
(B : Matrix n n R)
:
(kroneckerMap (fun (x1 x2 : R) => x1 * x2) A B).det = A.det ^ Fintype.card n * B.det ^ Fintype.card m
theorem
Matrix.conjTranspose_kronecker
{R : Type u_1}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommMagma R]
[StarMul R]
(x : Matrix l m R)
(y : Matrix n p R)
:
(kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y).conjTranspose = kroneckerMap (fun (x1 x2 : R) => x1 * x2) x.conjTranspose y.conjTranspose
theorem
Matrix.conjTranspose_kronecker'
{R : Type u_1}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[Mul R]
[StarMul R]
(x : Matrix l m R)
(y : Matrix n p R)
:
(kroneckerMap (fun (x1 x2 : R) => x1 * x2) x y).conjTranspose = (kroneckerMap (fun (x1 x2 : R) => x1 * x2) y.conjTranspose x.conjTranspose).submatrix Prod.swap Prod.swap
Specialization to Matrix.kroneckerMap (⊗ₜ) #
def
Matrix.kroneckerTMul
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
:
The Kronecker tensor product. This is just a shorthand for kroneckerMap (⊗ₜ).
Prefer the notation ⊗ₖₜ rather than this definition.
Equations
- Matrix.kroneckerTMul R = Matrix.kroneckerMap fun (x1 : α) (x2 : β) => x1 ⊗ₜ[R] x2
Instances For
The Kronecker tensor product. This is just a shorthand for kroneckerMap (⊗ₜ).
Prefer the notation ⊗ₖₜ rather than this definition.
Equations
- Kronecker.«term_⊗ₖₜ_» = Lean.ParserDescr.trailingNode `Kronecker.«term_⊗ₖₜ_» 100 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₖₜ ") (Lean.ParserDescr.cat `term 101))
Instances For
The Kronecker tensor product. This is just a shorthand for kroneckerMap (⊗ₜ).
Prefer the notation ⊗ₖₜ rather than this definition.
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_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(A : Matrix l m α)
(B : Matrix n p β)
(i₁ : l)
(i₂ : n)
(j₁ : m)
(j₂ : p)
:
def
Matrix.kroneckerTMulBilinear
(R : Type u_1)
(S : Type u_2)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[Semiring S]
[Module S α]
[SMulCommClass R S α]
:
Matrix.kronecker as a bilinear map.
Equations
Instances For
@[simp]
theorem
Matrix.kroneckerTMulBilinear_apply
(R : Type u_1)
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[Semiring S]
[Module S α]
[SMulCommClass R S α]
(A : Matrix l m α)
(B : Matrix n p β)
:
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_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(B : Matrix n p β)
:
theorem
Matrix.kroneckerTMul_zero
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(A : Matrix l m α)
:
theorem
Matrix.add_kroneckerTMul
(R : Type u_1)
{α : Type u_3}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[Module R α]
(A₁ A₂ : Matrix l m α)
(B : Matrix n p α)
:
kroneckerMap (TensorProduct.tmul R) (A₁ + A₂) B = kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A₁ B + kroneckerMap (fun (x1 x2 : α) => x1 ⊗ₜ[R] x2) A₂ B
theorem
Matrix.kroneckerTMul_add
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
(A : Matrix l m α)
(B₁ B₂ : Matrix n p β)
:
kroneckerMap (TensorProduct.tmul R) A (B₁ + B₂) = kroneckerMap (fun (x1 : α) (x2 : β) => x1 ⊗ₜ[R] x2) A B₁ + kroneckerMap (fun (x1 : α) (x2 : β) => x1 ⊗ₜ[R] x2) A B₂
theorem
Matrix.smul_kroneckerTMul
(R : Type u_1)
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[Monoid S]
[DistribMulAction S α]
[SMulCommClass R S α]
(r : S)
(A : Matrix l m α)
(B : Matrix n p β)
:
theorem
Matrix.kroneckerTMul_smul
(R : Type u_1)
{S : Type u_2}
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[Monoid S]
[DistribMulAction S α]
[DistribMulAction S β]
[SMul S R]
[SMulCommClass R S α]
[IsScalarTower S R α]
[IsScalarTower S R β]
(r : S)
(A : Matrix l m α)
(B : Matrix n p β)
:
theorem
Matrix.single_kroneckerTMul_single
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[DecidableEq p]
(i₁ : l)
(j₁ : m)
(i₂ : n)
(j₂ : p)
(a : α)
(b : β)
:
@[deprecated Matrix.single_kroneckerTMul_single (since := "2025-05-05")]
theorem
Matrix.stdBasisMatrix_kroneckerTMul_stdBasisMatrix
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[DecidableEq l]
[DecidableEq m]
[DecidableEq n]
[DecidableEq p]
(i₁ : l)
(j₁ : m)
(i₂ : n)
(j₂ : p)
(a : α)
(b : β)
:
Alias of Matrix.single_kroneckerTMul_single.
theorem
Matrix.diagonal_kroneckerTMul_diagonal
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{m : Type u_10}
{n : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[DecidableEq m]
[DecidableEq n]
(a : m → α)
(b : n → β)
:
kroneckerMap (TensorProduct.tmul R) (diagonal a) (diagonal b) = diagonal fun (mn : m × n) => a mn.1 ⊗ₜ[R] b mn.2
theorem
Matrix.kroneckerTMul_diagonal
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[DecidableEq n]
(A : Matrix l m α)
(b : n → β)
:
kroneckerMap (TensorProduct.tmul R) A (diagonal b) = blockDiagonal fun (i : n) => A.map fun (a : α) => a ⊗ₜ[R] b i
theorem
Matrix.diagonal_kroneckerTMul
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[DecidableEq l]
(a : l → α)
(B : Matrix m n β)
:
kroneckerMap (TensorProduct.tmul R) (diagonal a) B = (reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (blockDiagonal fun (i : l) => B.map fun (b : β) => a i ⊗ₜ[R] b)
theorem
Matrix.kroneckerTMul_assoc
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
{q : Type u_13}
{r : Type u_14}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(A : Matrix l m α)
(B : Matrix n p β)
(C : Matrix q r γ)
:
(reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r))
((kroneckerMap (TensorProduct.tmul R) (kroneckerMap (TensorProduct.tmul R) A B) C).map
⇑(TensorProduct.assoc R α β γ)) = kroneckerMap (TensorProduct.tmul R) A (kroneckerMap (TensorProduct.tmul R) B C)
@[simp]
theorem
Matrix.kroneckerTMul_assoc'
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{γ : Type u_7}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{p : Type u_12}
{q : Type u_13}
{r : Type u_14}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[AddCommMonoid γ]
[Module R α]
[Module R β]
[Module R γ]
(A : Matrix l m α)
(B : Matrix n p β)
(C : Matrix q r γ)
:
((kroneckerMap (TensorProduct.tmul R) (kroneckerMap (TensorProduct.tmul R) A B) C).map
⇑(TensorProduct.assoc R α β γ)).submatrix
⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = kroneckerMap (TensorProduct.tmul R) A (kroneckerMap (TensorProduct.tmul R) B C)
theorem
Matrix.trace_kroneckerTMul
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{m : Type u_10}
{n : Type u_11}
[CommSemiring R]
[AddCommMonoid α]
[AddCommMonoid β]
[Module R α]
[Module R β]
[Fintype m]
[Fintype n]
(A : Matrix m m α)
(B : Matrix n n β)
:
@[simp]
theorem
Matrix.one_kroneckerTMul_one
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{m : Type u_10}
{n : Type u_11}
[CommSemiring R]
[AddCommMonoidWithOne α]
[AddCommMonoidWithOne β]
[Module R α]
[Module R β]
[DecidableEq m]
[DecidableEq n]
:
theorem
Matrix.mul_kroneckerTMul_mul
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{l : Type u_9}
{m : Type u_10}
{n : Type u_11}
{l' : Type u_15}
{m' : Type u_16}
{n' : Type u_17}
[CommSemiring R]
[NonUnitalSemiring α]
[NonUnitalSemiring β]
[Module R α]
[Module R β]
[IsScalarTower R α α]
[SMulCommClass R α α]
[IsScalarTower R β β]
[SMulCommClass R β β]
[Fintype m]
[Fintype m']
(A : Matrix l m α)
(B : Matrix m n α)
(A' : Matrix l' m' β)
(B' : Matrix m' n' β)
:
kroneckerMap (TensorProduct.tmul R) (A * B) (A' * B') = kroneckerMap (TensorProduct.tmul R) A A' * kroneckerMap (TensorProduct.tmul R) B B'
theorem
Matrix.det_kroneckerTMul
(R : Type u_1)
{α : Type u_3}
{β : Type u_5}
{m : Type u_10}
{n : Type u_11}
[CommRing R]
[CommRing α]
[CommRing β]
[Algebra R α]
[Algebra R β]
[Fintype m]
[Fintype n]
[DecidableEq m]
[DecidableEq n]
(A : Matrix m m α)
(B : Matrix n n β)
:
(kroneckerMap (TensorProduct.tmul R) A B).det = (A.det ^ Fintype.card n) ⊗ₜ[R] (B.det ^ Fintype.card m)