Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-09-26 06:47
a8c41d02
View on Github →
feat(LinearAlgebra): trace of
LinearMap.smulRight
(
#29890
) from
PhysLean
Estimated changes
Modified
Mathlib/LinearAlgebra/Matrix/ToLin.lean
added
theorem
LinearMap.toMatrix_smulRight
Modified
Mathlib/LinearAlgebra/Trace.lean
added
theorem
LinearMap.trace_smulRight