mathlib

880c7bd4 - chore(linear_algebra/matrix): add fin expansions for trace and adjugate, and some trace lemmas (#9884)

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.