Equivalent_Matrices_Equal_Rank

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

linear-algebramatrixproofwikirank

Let $\mathbf A$ and $\mathbf B$ be $m \times n$ matrices over a field $K$ . Let $\map \phi {\mathbf A}$ denote the rank of $\mathbf A$ . Let $\mathbf A \equiv \mathbf B$ denote that $\mathbf A$ and $\mathbf B$ are matrix equivalent. Then $\mathbf A \equiv \mathbf B$ $\map \phi {\mathbf A} = \map \phi {\mathbf B}$

Preamble

import Mathlib.LinearAlgebra.Matrix.ToLin
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Dimension.Finrank

Formal statement

theorem Equivalent_Matrices_Equal_Rank {K : Type _} [Field K] [DecidableEq K] {m n : ℕ} (A B : Matrix (Fin m) (Fin n) K) (P : Matrix (Fin n) (Fin n) K) (Q : Matrix (Fin m) (Fin m) K) (hP : IsUnit P) (hQ : IsUnit Q) (h : B = Q * A * P⁻¹) : Module.finrank K (LinearMap.range A.toLin') = Module.finrank K (LinearMap.range B.toLin') := by sorry

Source

https://proofwiki.org/wiki/Equivalent_Matrices_have_Equal_Rank

View graph