rank_conjTranspose — Mathlib

English

The rank of the conjugate transpose A* equals the rank of A.

Русский

Ранк сопряжённого транспонирования матрицы A равен рангу A.

LaTeX

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

Lean4

/-- TODO: prove this in greater generality. -/
@[simp]
theorem rank_conjTranspose (A : Matrix m n R) : Aᴴ.rank = A.rank :=
  le_antisymm
    (((rank_conjTranspose_mul_self _).symm.trans_le <| rank_mul_le_left _ _).trans_eq <|
      congr_arg _ <| conjTranspose_conjTranspose _)
    ((rank_conjTranspose_mul_self _).symm.trans_le <| rank_mul_le_left _ _)

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