feat: Mul by invertible matrices is injective even for rectangular ma…

…trices (#6486)

Multiplication by invertible matrices from the left or right is injective. Note that [`mul_left_injective₀`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/GroupWithZero/Defs.html#mul_left_injective%E2%82%80) and friends don't apply because they would require similar (square) matrices.

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

@@ -356,6 +356,20 @@ theorem mul_inv_eq_iff_eq_mul_of_invertible (A B C : Matrix n n α) [Invertible
    fun h => by rw [h, mul_inv_cancel_right_of_invertible]⟩
 #align matrix.mul_inv_eq_iff_eq_mul_of_invertible Matrix.mul_inv_eq_iff_eq_mul_of_invertible
 
+lemma mul_right_injective_of_invertible [Invertible A] :
+    Function.Injective (fun (x : Matrix n m α) => A ⬝ x) :=
+  fun _ _ h => by simpa only [inv_mul_cancel_left_of_invertible] using congr_arg (A⁻¹ ⬝ ·) h
+
+lemma mul_left_injective_of_invertible [Invertible A] :
+    Function.Injective (fun (x : Matrix m n α) => x ⬝ A) :=
+  fun a x hax => by simpa only [mul_inv_cancel_right_of_invertible] using congr_arg (· ⬝ A⁻¹) hax
+
+lemma mul_right_inj_of_invertible [Invertible A] {x y : Matrix n m α} : A ⬝ x = A ⬝ y ↔ x = y :=
+  (mul_right_injective_of_invertible A).eq_iff
+
+lemma mul_left_inj_of_invertible [Invertible A] {x y : Matrix m n α} : x ⬝ A = y ⬝ A ↔ x = y :=
+  (mul_left_injective_of_invertible A).eq_iff
+
 theorem nonsing_inv_cancel_or_zero : A⁻¹ ⬝ A = 1 ∧ A ⬝ A⁻¹ = 1 ∨ A⁻¹ = 0 := by
   by_cases h : IsUnit A.det
   · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩