Similar_Matrices_are_Equivalent
Provedlinear-algebramatrixproofwikisimilarity
If two square matrices over a ring with unity are similar, then they are equivalent. It follows directly that every equivalence class for the relation of similarity on is contained in an equivalence class for the relation of matrix equivalence. Here, denotes the matrix space over .
Preamble
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Formal statement
theorem Similar_Matrices_are_Equivalent {R : Type _} [CommRing R] {n : ℕ} (A B : Matrix (Fin n) (Fin n) R) (P : Matrix (Fin n) (Fin n) R) (hP : IsUnit P) (h : B = P * A * P⁻¹) : ∃ (Q S : Matrix (Fin n) (Fin n) R), IsUnit Q ∧ IsUnit S ∧ B = Q * A * S⁻¹ := by sorrySource