Theorems · Definition · linear algebra
LinearMap.trace
(R : Type u) → [inst : CommSemiring R] → (M : Type v) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] M) →ₗ[R] R
Trace of an endomorphism independent of basis.
- Defined in
- Mathlib.LinearAlgebra.Trace
- Cited by
- 87 results in Mathlib
- Foundations
- Depth 89 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement · cited by 18,349
- Finsetproof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- LinearMapstatement · cited by 10,215
- Module.Basisproof · cited by 1,477
- Nonempty.someproof · cited by 340
- LinearMap.traceAuxproof · cited by 6
Cited by92
Results whose statement or proof uses this declaration.
- Algebra.traceproof · cited by 90
- LieModule.traceFormproof · cited by 41
- LinearMap.trace_eq_matrix_tracestatement · cited by 14
- FDRep.characterproof · cited by 11
- Representation.characterproof · cited by 10
- LinearMap.trace_conj'statement and proof · cited by 8
- LinearMap.trace_mul_commstatement and proof · cited by 8
- LieModule.traceForm_apply_applystatement · cited by 6
- LinearMap.isNilpotent_trace_of_isNilpotentstatement · cited by 5
- LieModule.traceForm_apply_lie_applyproof · cited by 5
- LinearMap.trace_eq_contract_applystatement and proof · cited by 5
- Algebra.trace_eq_of_algEquivproof · cited by 4