Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.det_is_unit_smul

Modification history

2022-01-04 07:46
src/linear_algebra/determinant.lean
feat(linear_algebra/determinant): `det_units_smul` and `det_is_unit_smul` (#11206) …
Added basis.det_is_unit_smulView on Github →