mathlib3

b94ea159 - refactor(linear_algebra/matrix/trace): unbundle `matrix.diag` (#13687)

refactor(linear_algebra/matrix/trace): unbundle `matrix.diag` (#13687) The bundling makes it awkward to work with, as the base ring has to be specified even though it doesn't affect the computation. This brings it in line with `matrix.diagonal`. The bundled version is now available as `matrix.diag_linear_map`. This adds a handful of missing lemmas about `diag` inspired by those about `diagonal`; almost all of which are just `rfl`.