Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-05 17:24 77e1e3b2

View on Github →

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

Estimated changes

Modified src/linear_algebra/matrix/nonsingular_inverse.lean

added def matrix.det_invertible_of_invertible

added def matrix.det_invertible_of_left_inverse

added def matrix.det_invertible_of_right_inverse

added def matrix.invertible_of_det_invertible

added def matrix.unit_of_det_invertible

added theorem matrix.unit_of_det_invertible_eq_nonsing_inv_unit