Theorems · Theorem · linear algebra

Matrix.toLin_kronecker

∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_5} {N' : Type u_6} {ι : Type u_7} {κ : Type u_8}
  {ι' : Type u_10} {κ' : Type u_11} [inst : DecidableEq ι] [inst_1 : DecidableEq κ] [inst_2 : Fintype ι]
  [inst_3 : Fintype κ] [inst_4 : Finite ι'] [inst_5 : Finite κ'] [inst_6 : CommRing R] [inst_7 : AddCommGroup M]
  [inst_8 : AddCommGroup N] [inst_9 : AddCommGroup M'] [inst_10 : AddCommGroup N'] [inst_11 : Module R M]
  [inst_12 : Module R N] [inst_13 : Module R M'] [inst_14 : Module R N'] (bM : Module.Basis ι R M)
  (bN : Module.Basis κ R N) (bM' : Module.Basis ι' R M') (bN' : Module.Basis κ' R N') (A : Matrix ι' ι R)
  (B : Matrix κ' κ R),
  (Matrix.toLin (bM.tensorProduct bN) (bM'.tensorProduct bN')) (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B) =
    TensorProduct.map ((Matrix.toLin bM bM') A) ((Matrix.toLin bN bN') B)

The matrix built from Matrix.kronecker corresponds to the linear map built from TensorProduct.map.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Matrix

Cited by

0 results in Mathlib

Foundations

Depth 95 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqDecidableEqFintypeFintypeFiniteFiniteCommRingAddCommGroupAddCommGroupAddCommGroupAddCommGroupModuleModuleModuleModule