no goals
l : Type ?u.188785
m : Type u_1
n : Type u_3
o : Type ?u.188794
R : Type u_2
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : CommRing R
inst✝ : Fintype m
A : Matrix m m R
e₁ e₂ : n ≃ m
⊢ rank (submatrix A ↑e₁ ↑e₂) = rank A
simpa only [reindex_apply] using rank_reindex e₁.symm e₂.symm A