Theorems · Theorem · commutative algebra

Algebra.traceMatrix_apply

∀ {κ : Type w} (A : Type u) {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (b : κ → B)
  (i j : κ), Algebra.traceMatrix A b i j = ((Algebra.traceForm A B) (b i)) (b j)

Defined in

Mathlib.RingTheory.Trace.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra