Mathlib v3 is deprecated. Go to Mathlib v4

Theorem basis.det_units_smul

Modification history

2022-09-30 23:37
src/linear_algebra/determinant.lean
feat(linear_algebra/{basis, determinant, orientation}): determinant of `adjust_to_orientation` of a basis (#16476) …
Modified basis.det_units_smulView on Github →
2022-01-05 23:45
src/linear_algebra/determinant.lean
chore(*): notation for `units` (#11236)
Modified basis.det_units_smulView on Github →
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_units_smulView on Github →