English
The rank of A* A is equal to the rank of A, for matrices over appropriate fields with the relevant order and involution structure.
Русский
Ранк матрицы A* A равен рангу матрицы A при подходящих условиях поля и инволюции.
LaTeX
$$$ \operatorname{rank}(A^{*} A) = \operatorname{rank}(A). $$$
Lean4
theorem rank_conjTranspose_mul_self (A : Matrix m n R) : (Aᴴ * A).rank = A.rank :=
by
dsimp only [rank]
refine add_left_injective (finrank R (LinearMap.ker (mulVecLin A))) ?_
dsimp only
trans
finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᴴ * A)) } +
finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᴴ * A)) }
· rw [ker_mulVecLin_conjTranspose_mul_self]
·
simp only [LinearMap.finrank_range_add_finrank_ker]
-- this follows the proof here https://math.stackexchange.com/a/81903/1896
