Theorems · Definition · commutative algebra

Algebra.traceMatrix

{κ : Type w} →
  (A : Type u) → {B : Type v} → [inst : CommRing A] → [inst_1 : CommRing B] → [Algebra A B] → (κ → B) → Matrix κ κ A

Given an A-algebra B and b, a κ-indexed family of elements of B, we define traceMatrix A b as the matrix whose (i j)-th element is the trace of b i * b j.

Defined in

Mathlib.RingTheory.Trace.Basic

Cited by

24 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra