Commit 2021-10-25 20:31 880c7bd4

View on Github →

chore(linear_algebra/matrix): add fin expansions for trace and adjugate, and some trace lemmas (#9884) We have these expansions for det already, I figured we may as well have them for these. This adds some other trivial trace lemmas while I'm touching the same file.

Estimated changes

Modified src/algebra/lie/classical.lean

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

added theorem matrix.adjugate_fin_one

added theorem matrix.adjugate_fin_zero

Modified src/linear_algebra/matrix/trace.lean

added theorem matrix.diag_col_mul_row

added theorem matrix.trace_col_mul_row

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_mul_cycle'

added theorem matrix.trace_mul_cycle