mathlib

320df450 - refactor(linear_algebra/trace): unbundle `matrix.trace` (#13712)

refactor(linear_algebra/trace): unbundle `matrix.trace` (#13712) These extra type arguments are annoying to work with in many cases, especially when Lean doesn't have any information to infer the mostly-irrelevant `R` argument from. This came up while trying to work with `continuous.matrix_trace`, which is annoying to use for that reason. The old bundled version is still available as `matrix.trace_linear_map`. The cost of this change is that we have to copy across the usual set of obvious lemmas about additive maps; but we already do this for `diagonal`, `transpose` etc anyway.