Matrix_Equivalence_is_Equivalence_Relation

import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

theorem Matrix_Equivalence_is_Equivalence_Relation {R : Type _} [CommRing R] {m n : ℕ} : Equivalence (fun A B : Matrix (Fin m) (Fin n) R => ∃ (P : Matrix (Fin n) (Fin n) R) (Q : Matrix (Fin m) (Fin m) R), IsUnit P ∧ IsUnit Q ∧ B = Q * A * P⁻¹) := by sorry