Theorem LinearMap.trace_smulRight

Modification history

2025-09-26 06:47

Mathlib/LinearAlgebra/Trace.lean

feat(LinearAlgebra): trace of `LinearMap.smulRight` (#29890) …

Added LinearMap.trace_smulRight View on Github →