Theorem LinearMap.trace_tensorProduct

Modification history

2025-10-30 11:10

Mathlib/LinearAlgebra/Trace.lean

chore(LinearAlgebra/TensorProduct/Basic): more semi-linearizing (#27353)

Modified LinearMap.trace_tensorProduct View on Github →

2023-05-23 11:38

Mathlib/LinearAlgebra/Trace.lean

feat: port LinearAlgebra.Trace (#4264)

Added LinearMap.trace_tensorProduct View on Github →