no goals
l : Type ?u.262172
m : Type u_1
n : Type u_2
o : Type ?u.262181
R : Type u_3
m_fin : Fintype m
inst✝⁵ : Fintype n
inst✝⁴ : Fintype o
inst✝³ : Fintype m
inst✝² : Field R
inst✝¹ : PartialOrder R
inst✝ : StarOrderedRing R
A : Matrix m n R
⊢ rank (A ⬝ Aᴴ) = rank A
simpa only [rank_conjTranspose, conjTranspose_conjTranspose] using
  rank_conjTranspose_mul_self Aᴴ