Theorems · Theorem · linear algebra

Matrix.trace_kroneckerMapBilinear

∀ {R : Type u_1} {S : Type u_2} {α : Type u_3} {β : Type u_5} {γ : Type u_7} {m : Type u_10} {n : Type u_11}
  [inst : Semiring S] [inst_1 : Semiring R] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : AddCommMonoid α]
  [inst_5 : AddCommMonoid β] [inst_6 : AddCommMonoid γ] [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 : Matrix m m α) (B : Matrix n n β), (((Matrix.kroneckerMapBilinear f) A) B).trace = (f A.trace) B.trace

trace distributes over Matrix.kroneckerMapBilinear. This is primarily used with R = ℕ to prove Matrix.trace_kronecker.

Defined in

Mathlib.LinearAlgebra.Matrix.Kronecker

Cited by

2 results in Mathlib

Foundations

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

Assumes

SemiringSemiringFintypeFintypeAddCommMonoidAddCommMonoidAddCommMonoidModuleModuleModuleModuleSMulCommClass