Commit 2023-04-02 23:34 1c65b428

View on Github →

feat: port LinearAlgebra.Matrix.Trace (#3231)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Trace.lean

added def Matrix.trace

added def Matrix.traceAddMonoidHom

added def Matrix.traceLinearMap

added theorem Matrix.trace_add

added theorem Matrix.trace_col_mul_row

added theorem Matrix.trace_conjTranspose

added theorem Matrix.trace_fin_one

added theorem Matrix.trace_fin_three

added theorem Matrix.trace_fin_two

added theorem Matrix.trace_fin_zero

added theorem Matrix.trace_list_sum

added theorem Matrix.trace_mul_comm

added theorem Matrix.trace_mul_cycle'

added theorem Matrix.trace_mul_cycle

added theorem Matrix.trace_multiset_sum

added theorem Matrix.trace_neg

added theorem Matrix.trace_one

added theorem Matrix.trace_smul

added theorem Matrix.trace_sub

added theorem Matrix.trace_sum

added theorem Matrix.trace_transpose

added theorem Matrix.trace_transpose_mul

added theorem Matrix.trace_zero