Mathlib v3 is deprecated. Go to Mathlib v4

Def matrix.det_invertible_of_invertible

Modification history

2021-07-05 17:24

src/linear_algebra/matrix/nonsingular_inverse.lean

feat(linear_algebra/nonsingular_inverse): add lemmas about `invertible` (#8201)

Added matrix.det_invertible_of_invertible View on Github →