Theorems · Theorem · commutative algebra

Algebra.traceMatrix_of_matrix_mulVec

∀ {κ : 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 ((P.map ⇑(algebraMap A B)).mulVec b) = P * Algebra.traceMatrix A b * P.transpose

Defined in

Mathlib.RingTheory.Trace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFintype