Theorems · Theorem · linear algebra

LinearMap.trace_eq_contract

∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M], LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M

When M is finite free, the trace of a linear map corresponds to the contraction pairing under the isomorphism End(M) ≃ M* ⊗ M.

Defined in

Mathlib.LinearAlgebra.Trace

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleModule.FreeModule.Finite