Theorems · Theorem · commutative algebra

Algebra.traceMatrix_of_basis

∀ {κ : Type w} {A : Type u} {B : Type v} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Fintype κ] [inst_4 : DecidableEq κ] (b : Module.Basis κ A B),
  Algebra.traceMatrix A ⇑b = (LinearMap.BilinForm.toMatrix b) (Algebra.traceForm A B)

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

CommRingCommRingAlgebraFintypeDecidableEq