rank_transpose_mul_self — Mathlib

English

Rank of A* A equals rank of A (same as conjTranspose case).

Русский

Ранк A* A равен рангу A.

LaTeX

$$$ \operatorname{rank}(A^{*} A) = \operatorname{rank}(A). $$$

Lean4

theorem rank_transpose_mul_self (A : Matrix m n R) : (Aᵀ * A).rank = A.rank :=
  by
  dsimp only [rank]
  refine add_left_injective (finrank R <| LinearMap.ker A.mulVecLin) ?_
  dsimp only
  trans
    finrank R { x // x ∈ LinearMap.range (mulVecLin (Aᵀ * A)) } +
      finrank R { x // x ∈ LinearMap.ker (mulVecLin (Aᵀ * A)) }
  · rw [ker_mulVecLin_transpose_mul_self]
  · simp only [LinearMap.finrank_range_add_finrank_ker]

Похожие утверждения