Commit 2022-05-02 11:44 320df450

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.