Theorems · Theorem · linear algebra

Matrix.trace_mul_cycle

∀ {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n]
  [inst_2 : Fintype p] [inst_3 : NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R),
  (A * B * C).trace = (C * A * B).trace

Defined in

Mathlib.LinearAlgebra.Matrix.Trace

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeFintypeFintypeNonUnitalCommSemiring