Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.det_smul

Modification history

2021-09-13 16:19

src/linear_algebra/determinant.lean

feat(linear_algebra/determinant): more on the determinant of linear maps (#9139)

Added linear_map.det_smul View on Github →