Commit 2023-08-10 21:26 96a37689

View on Github →

feat: Mul by invertible matrices is injective even for rectangular matrices (#6486) Multiplication by invertible matrices from the left or right is injective. Note that mul_left_injective₀ and friends don't apply because they would require similar (square) matrices.

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.mul_left_inj_of_invertible

added theorem Matrix.mul_left_injective_of_invertible

added theorem Matrix.mul_right_inj_of_invertible

added theorem Matrix.mul_right_injective_of_invertible