mathlib3

85784b05 - feat(linear_algebra/determinant): `det_units_smul` and `det_is_unit_smul` (#11206)

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.