no goals
l : Type ?u.284550
m : Type u_1
n : Type u_2
o : Type ?u.284559
R : Type u_3
m_fin : Fintype m
inst✝³ : Fintype n
inst✝² : Fintype o
inst✝¹ : Fintype m
inst✝ : LinearOrderedField R
A : Matrix m n R
⊢ rank (A ⬝ Aᵀ) = rank A
simpa only [rank_transpose, transpose_transpose] using rank_transpose_mul_self Aᵀ