Row_Equivalence_is_Equivalence_Relation_v2

import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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