Commit 2022-04-26 09:51 b94ea159
View on Github →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.