rank_self_mul_conjTranspose — Mathlib

English

The kernel of (A^T A) acting on vectors equals the kernel of A acting on vectors.

Русский

Ядро (A^T A) при умножении на вектор совпадает с ядром A при умножении на вектор.

LaTeX

$$$ \ker\big(A^{T} A\big) \cdot \text{mulVecLin} = \ker\big(A\,\mathrm{mulVecLin}\big). $$$

Lean4

@[simp]
theorem rank_self_mul_conjTranspose (A : Matrix m n R) : (A * Aᴴ).rank = A.rank := by
  simpa only [rank_conjTranspose, conjTranspose_conjTranspose] using rank_conjTranspose_mul_self Aᴴ

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