Commit 2022-01-03 14:30 236d978d
View on Github →feat(linear_algebra/matrix/basis): to_matrix_units_smul and to_matrix_is_unit_smul (#11191)
Add lemmas that applying to_matrix to a basis constructed with
units_smul or is_unit_smul produces the corresponding diagonal
matrix.