Theorems · Definition · linear algebra

LinearMap.traceAux

(R : Type u) →
  [inst : CommSemiring R] →
    {M : Type v} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → {ι : Type w} → [DecidableEq ι] → [Fintype ι] → Module.Basis ι R M → (M →ₗ[R] M) →ₗ[R] R

The trace of an endomorphism given a basis.

Defined in

Mathlib.LinearAlgebra.Trace

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleDecidableEqFintype