ker_mulVecLin_transpose_mul_self — Mathlib

English

Same kernel equality as in the transpose case, possibly with A^T.

Русский

Та же равенство ядер для варианта с транспонированием.

LaTeX

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

Lean4

theorem ker_mulVecLin_transpose_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, ← mulVec_mulVec]
  constructor
  · intro h
    replace h := congr_arg (dotProduct x) h
    rwa [dotProduct_mulVec, dotProduct_zero, vecMul_transpose, dotProduct_self_eq_zero] at h
  · intro h
    rw [h, mulVec_zero]

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