Theorems · Definition · linear algebra

Matrix.kroneckerTMulStarAlgEquiv

(m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_5) →
      (S : Type u_6) →
        (A : Type u_7) →
          (B : Type u_8) →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Semiring B] →
                  [inst_3 : Algebra R A] →
                    [inst_4 : Algebra R B] →
                      [inst_5 : Fintype n] →
                        [inst_6 : DecidableEq n] →
                          [inst_7 : CommSemiring S] →
                            [inst_8 : Algebra R S] →
                              [inst_9 : Algebra S A] →
                                [inst_10 : IsScalarTower R S A] →
                                  [inst_11 : Fintype m] →
                                    [inst_12 : DecidableEq m] →
                                      [inst_13 : StarRing R] →
                                        [inst_14 : StarAddMonoid A] →
                                          [inst_15 : StarAddMonoid B] →
                                            [inst_16 : StarModule R A] →
                                              [inst_17 : StarModule R B] →
                                                TensorProduct R (Matrix m m A) (Matrix n n B) ≃⋆ₐ[S]
                                                  Matrix (m × n) (m × n) (TensorProduct R A B)

Matrix.kroneckerTMul as a ⋆-algebra equivalence, when the two arguments are tensored.

Defined in

Mathlib.RingTheory.MatrixAlgebra

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringSemiringAlgebraAlgebraFintypeDecidableEqCommSemiringAlgebraAlgebraIsScalarTowerFintypeDecidableEqStarRingStarAddMonoidStarAddMonoidStarModuleStarModule