ker_mulVecLin_conjTranspose_mul_self

English

For a matrix A over a field with an involution structure, the kernel of (A* A) acting by left multiplication on vectors equals the kernel of A acting by left multiplication on vectors.

Русский

Для матрицы A над полем с инволютивной структурой ядро (A* A) при умножении на вектор совпадает с ядром A при умножении на вектор.

LaTeX

$$$ \ker\big(A^{*} A\big) \cdot \text{mulVecLin} = \ker\big(\text{mulVecLin } A\big). $$$

Lean4

theorem ker_mulVecLin_conjTranspose_mul_self (A : Matrix m n R) :
    LinearMap.ker (Aᴴ * A).mulVecLin = LinearMap.ker (mulVecLin A) :=
  by
  ext x
  simp only [LinearMap.mem_ker, mulVecLin_apply, conjTranspose_mul_self_mulVec_eq_zero]

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