Theorems · Theorem · linear algebra

kroneckerLinearEquiv_tmul

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_5} [inst : CommSemiring R]
  [inst_1 : Fintype l] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Fintype p] [inst_5 : DecidableEq l]
  [inst_6 : DecidableEq m] [inst_7 : DecidableEq n] [inst_8 : DecidableEq p] (x : Matrix l m R) (y : Matrix n p R),
  (kroneckerLinearEquiv l m n p R) (x ⊗ₜ[R] y) = Matrix.kroneckerMap (fun x1 x2 => x1 * x2) x y

Defined in

Mathlib.RingTheory.MatrixAlgebra

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringFintypeFintypeFintypeFintypeDecidableEqDecidableEqDecidableEqDecidableEq