mathlib

236d978d - feat(linear_algebra/matrix/basis): `to_matrix_units_smul` and `to_matrix_is_unit_smul` (#11191)

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.