Mathlib v3 is deprecated. Go to Mathlib v4

Def matrix.unit_of_det_invertible

Modification history

2022-01-05 23:45
src/linear_algebra/matrix/nonsingular_inverse.lean
chore(*): notation for `units` (#11236)
Modified matrix.unit_of_det_invertibleView on Github →
2021-07-05 17:24
src/linear_algebra/matrix/nonsingular_inverse.lean
feat(linear_algebra/nonsingular_inverse): add lemmas about `invertible` (#8201)
Added matrix.unit_of_det_invertibleView on Github →