feat: injectivity of multiplication with matrices whose product is 1 (#…

…7266)

Given two matrices $A$ and $B$ whose product is 1 $AB = 1$, then left multiplication/right multiplication with these matrices from the appropriate side is an injection.

Suggested by @Vierkantor  in PR #6042

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

@@ -347,6 +347,20 @@ lemma mul_right_inj_of_invertible [Invertible A] {x y : Matrix n m α} : A * x =
 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
 
+section InjectiveMul
+variable [Fintype m] [DecidableEq m]
+variable [Fintype l] [DecidableEq l]
+
+lemma mul_left_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
+    Function.Injective (fun x : Matrix l m α => x * A) :=
+  fun _ _ g => by simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g
+
+lemma mul_right_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) :
+    Function.Injective (fun x : Matrix m l α => B * x) :=
+  fun _ _ g => by simpa only [← Matrix.mul_assoc, Matrix.one_mul, h] using congr_arg (A * ·) g
+
+end InjectiveMul
+
 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⟩