Theorems · Theorem · linear algebra

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} [inst : Semiring S] [inst_1 : Semiring R]
  [inst_2 : Fintype m] [inst_3 : Fintype m'] [inst_4 : NonUnitalNonAssocSemiring α]
  [inst_5 : NonUnitalNonAssocSemiring β] [inst_6 : NonUnitalNonAssocSemiring γ] [inst_7 : Module R α]
  [inst_8 : Module R γ] [inst_9 : Module S β] [inst_10 : Module S γ] [inst_11 : SMulCommClass S R γ]
  (f : α →ₗ[R] β →ₗ[S] γ),
  (∀ (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' β),
      ((Matrix.kroneckerMapBilinear f) (A * B)) (A' * B') =
        ((Matrix.kroneckerMapBilinear f) A) A' * ((Matrix.kroneckerMapBilinear f) B) B'

Matrix.kroneckerMapBilinear commutes with * if f does. This is primarily used with R = ℕ to prove Matrix.mul_kronecker_mul.

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringSemiringFintypeFintypeNonUnitalNonAssocSemiringNonUnitalNonAssocSemiringNonUnitalNonAssocSemiringModuleModuleModuleModuleSMulCommClass