Commit 2023-05-23 11:38 1c9045fe

View on Github →

feat: port LinearAlgebra.Trace (#4264)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.IsProj.trace

added def LinearMap.trace

added def LinearMap.traceAux

added theorem LinearMap.traceAux_def

added theorem LinearMap.traceAux_eq

added theorem LinearMap.trace_comp_comm'

added theorem LinearMap.trace_comp_comm

added theorem LinearMap.trace_conj'

added theorem LinearMap.trace_conj

added theorem LinearMap.trace_eq_contract'

added theorem LinearMap.trace_eq_contract

added theorem LinearMap.trace_eq_contract_apply

added theorem LinearMap.trace_eq_contract_of_basis'

added theorem LinearMap.trace_eq_contract_of_basis

added theorem LinearMap.trace_eq_matrix_trace

added theorem LinearMap.trace_eq_matrix_trace_of_finset

added theorem LinearMap.trace_id

added theorem LinearMap.trace_mul_comm

added theorem LinearMap.trace_one

added theorem LinearMap.trace_prodMap'

added theorem LinearMap.trace_prodMap

added theorem LinearMap.trace_tensorProduct'

added theorem LinearMap.trace_tensorProduct

added theorem LinearMap.trace_transpose'

added theorem LinearMap.trace_transpose