Theorems · Definition · linear algebra

kroneckerLinearEquiv

(l : Type u_1) →
  (m : Type u_2) →
    (n : Type u_3) →
      (p : Type u_4) →
        (R : Type u_5) →
          [inst : CommSemiring R] →
            [Fintype l] →
              [Fintype m] →
                [Fintype n] →
                  [Fintype p] →
                    [DecidableEq l] →
                      [DecidableEq m] →
                        [DecidableEq n] →
                          [DecidableEq p] → TensorProduct R (Matrix l m R) (Matrix n p R) ≃ₗ[R] Matrix (l × n) (m × p) R

Matrix.kronecker as a linear equivalence, when the two arguments are tensored.

Defined in

Mathlib.RingTheory.MatrixAlgebra

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringFintypeFintypeFintypeFintypeDecidableEqDecidableEqDecidableEqDecidableEq