Theorems · Theorem · linear algebra
LinearMap.trace_mul_comm
∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f g : M →ₗ[R] M),
(LinearMap.trace R M) (f * g) = (LinearMap.trace R M) (g * f)- Defined in
- Mathlib.LinearAlgebra.Trace
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idstatement and proof · cited by 18,349
- Finsetproof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- CommSemiringstatement and proof · cited by 10,911
- LinearMapstatement and proof · cited by 10,215
- Module.Basisproof · cited by 1,477
- LinearMap.toMatrixproof · cited by 180
- Matrix.traceproof · cited by 114
- LinearMap.tracestatement and proof · cited by 87
- LinearMap.zero_applyproof · cited by 35
Cited by8
Results whose statement or proof uses this declaration.
- LieModule.traceForm_commproof · cited by 9
- LinearMap.trace_lieproof · cited by 3
- Representation.char_mul_commproof · cited by 1
- LinearMap.trace_lie_mul_eqproof · cited by 1
- LinearMap.trace_mul_cycle'proof · cited by 1
- FDRep.char_mul_commproof · cited by 1
- LinearMap.trace_mul_cycleproof · cited by 0
- LinearMap.trace_conjproof · cited by 0