Commit 2022-01-04 07:46 85784b05
View on Github →feat(linear_algebra/determinant): det_units_smul and det_is_unit_smul (#11206)
Add lemmas giving the determinant of a basis constructed with
units_smul or is_unit_smul with respect to the original basis.