Matrix_Similarity_is_Equivalence_Relation

import Mathlib.LinearAlgebra.Matrix.NonsingularInverse

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