Theorems · Theorem · linear algebra

Matrix.trace_single_mul

∀ {m : Type u_9} {n : Type u_10} {R : Type u_11} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : NonUnitalNonAssocSemiring R] [inst_4 : Fintype m] (i : n) (j : m) (a : R) (x : Matrix m n R),
  (Matrix.single i j a * x).trace = a • x j i

Defined in: Mathlib.LinearAlgebra.Matrix.Trace
Cited by: 1 results in Mathlib
Foundations: Depth 72 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: DecidableEq DecidableEq Fintype NonUnitalNonAssocSemiring Fintype

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Fintypestatement and proof · cited by 7,736
Finset.sumproof · cited by 5,195
Matrixstatement and proof · cited by 4,303
Finset.univproof · cited by 3,473
Finset.sum_congrproof · cited by 2,323
MulZeroClass.zero_mulproof · cited by 1,625
NonUnitalNonAssocSemiringstatement and proof · cited by 1,081
Matrix.ofproof · cited by 336
Finset.sum_const_zeroproof · cited by 219
Matrix.singlestatement · cited by 129
Matrix.tracestatement · cited by 114

Cited by1

Results whose statement or proof uses this declaration.

Matrix.ext_iff_trace_mul_leftproof · cited by 0