Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.det_fin_one_of

Modification history

2022-07-17 21:26

src/linear_algebra/matrix/determinant.lean

chore(linear_algebra/matrix): Use the new matrix notation in most places (#15306)

Added matrix.det_fin_one_of View on Github →