Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.unit_of_det_invertible_eq_nonsing_inv_unit

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.unit_of_det_invertible_eq_nonsing_inv_unit View on Github →