Commit 2023-12-08 12:43 31037d92

View on Github →

feat: Invertible matrices (#8219) We add some results on invertible matrices, showing that for a finite square matrix A, IsUnit A is equivalent to the surjectivity/injectivity of left/right multiplication, and to the linear independence of the set of rows/columns. We also add a couple of lemmas about the existence of left/right inverses for nonsquare matrices, and a bit of API for mulVecLin and vecMulLinear.

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

added theorem Matrix.mul_apply_eq_vecMul

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.exists_left_inverse_iff_isUnit

added theorem Matrix.exists_right_inverse_iff_isUnit

added theorem Matrix.linearIndependent_cols_iff_isUnit

added theorem Matrix.linearIndependent_cols_of_invertible

added theorem Matrix.linearIndependent_rows_iff_isUnit

added theorem Matrix.linearIndependent_rows_of_invertible

added theorem Matrix.mulVec_injective_iff_isUnit

added theorem Matrix.mulVec_injective_of_invertible

added theorem Matrix.mulVec_surjective_iff_exists_right_inverse

added theorem Matrix.mulVec_surjective_iff_isUnit

added theorem Matrix.mulVec_surjective_of_invertible

added theorem Matrix.vecMul_injective_iff_isUnit

added theorem Matrix.vecMul_injective_of_invertible

added theorem Matrix.vecMul_surjective_iff_exists_left_inverse

added theorem Matrix.vecMul_surjective_iff_isUnit

added theorem Matrix.vecMul_surjective_of_invertible

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

added theorem Matrix.coe_mulVecLin

added theorem Matrix.coe_vecMulLinear

modified theorem Matrix.ker_mulVecLin_eq_bot_iff

added theorem Matrix.mulVecLin_transpose

added theorem Matrix.mulVec_injective_iff

added theorem Matrix.vecMulLinear_apply

added theorem Matrix.vecMulLinear_transpose

added theorem Matrix.vecMul_injective_iff

added theorem range_vecMulLinear