Theorems · Theorem · commutative algebra

Algebra.traceMatrix_of_matrix_vecMul

∀ {κ : Type w} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Fintype κ] (b : κ → B) (P : Matrix κ κ A),
  Algebra.traceMatrix A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.transpose * Algebra.traceMatrix A b * P

Defined in

Mathlib.RingTheory.Trace.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFintype