Commit 2023-04-25 15:53 d8af7b4f

View on Github →

feat: port LinearAlgebra.Matrix.NonsingularInverse (#3647)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Units.lean

Modified Mathlib/Algebra/Invertible.lean

Created Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.coe_units_inv

added theorem Matrix.conjTranspose_nonsing_inv

added def Matrix.detInvertibleOfInvertible

added def Matrix.detInvertibleOfLeftInverse

added def Matrix.detInvertibleOfRightInverse

added theorem Matrix.det_conj'

added theorem Matrix.det_conj

added theorem Matrix.det_invOf

added theorem Matrix.det_ne_zero_of_left_inverse

added theorem Matrix.det_ne_zero_of_right_inverse

added theorem Matrix.det_nonsing_inv

added theorem Matrix.det_nonsing_inv_mul_det

added theorem Matrix.det_smul_inv_mulVec_eq_cramer

added theorem Matrix.det_smul_inv_vecMul_eq_cramer_transpose

added def Matrix.diagonalInvertible

added def Matrix.diagonalInvertibleEquivInvertible

added theorem Matrix.invOf_diagonal_eq

added theorem Matrix.invOf_eq

added theorem Matrix.invOf_eq_nonsing_inv

added theorem Matrix.invOf_submatrix_equiv_eq

added theorem Matrix.inv_adjugate

added theorem Matrix.inv_def

added theorem Matrix.inv_diagonal

added theorem Matrix.inv_eq_left_inv

added theorem Matrix.inv_eq_right_inv

added theorem Matrix.inv_inj

added theorem Matrix.inv_inv_inv

added theorem Matrix.inv_inv_of_invertible

added theorem Matrix.inv_mul_cancel_left_of_invertible

added theorem Matrix.inv_mul_cancel_right_of_invertible

added theorem Matrix.inv_mul_eq_iff_eq_mul_of_invertible

added theorem Matrix.inv_mul_of_invertible

added theorem Matrix.inv_reindex

added theorem Matrix.inv_smul'

added theorem Matrix.inv_smul

added theorem Matrix.inv_submatrix_equiv

added theorem Matrix.inv_zero

added def Matrix.invertibleEquivDetInvertible

added def Matrix.invertibleOfDetInvertible

added def Matrix.invertibleOfDiagonalInvertible

added def Matrix.invertibleOfInvertibleConjTranspose

added def Matrix.invertibleOfInvertibleTranspose

added def Matrix.invertibleOfLeftInverse

added def Matrix.invertibleOfRightInverse

added def Matrix.invertibleOfSubmatrixEquivInvertible

added theorem Matrix.isUnit_det_of_invertible

added theorem Matrix.isUnit_det_of_left_inverse

added theorem Matrix.isUnit_det_of_right_inverse

added theorem Matrix.isUnit_det_transpose

added theorem Matrix.isUnit_diagonal

added theorem Matrix.isUnit_iff_isUnit_det

added theorem Matrix.isUnit_nonsing_inv_det

added theorem Matrix.isUnit_nonsing_inv_det_iff

added theorem Matrix.isUnit_of_left_inverse

added theorem Matrix.isUnit_of_right_inverse

added theorem Matrix.isUnit_submatrix_equiv

added theorem Matrix.left_inv_eq_left_inv

added theorem Matrix.list_prod_inv_reverse

added theorem Matrix.mul_eq_one_comm

added theorem Matrix.mul_inv_cancel_left_of_invertible

added theorem Matrix.mul_inv_cancel_right_of_invertible

added theorem Matrix.mul_inv_eq_iff_eq_mul_of_invertible

added theorem Matrix.mul_inv_of_invertible

added theorem Matrix.mul_inv_rev

added theorem Matrix.mul_nonsing_inv

added theorem Matrix.mul_nonsing_inv_cancel_left

added theorem Matrix.mul_nonsing_inv_cancel_right

added theorem Matrix.nonsing_inv_apply

added theorem Matrix.nonsing_inv_apply_not_isUnit

added theorem Matrix.nonsing_inv_cancel_or_zero

added theorem Matrix.nonsing_inv_eq_ring_inverse

added theorem Matrix.nonsing_inv_mul

added theorem Matrix.nonsing_inv_mul_cancel_left

added theorem Matrix.nonsing_inv_mul_cancel_right

added theorem Matrix.nonsing_inv_nonsing_inv

added theorem Matrix.right_inv_eq_left_inv

added theorem Matrix.right_inv_eq_right_inv

added def Matrix.submatrixEquivInvertible

added def Matrix.submatrixEquivInvertibleEquivInvertible

added theorem Matrix.transpose_nonsing_inv

added def Matrix.unitOfDetInvertible

added theorem Matrix.unitOfDetInvertible_eq_nonsingInvUnit