conjTranspose_mul_self_mulVec_eq_zero

English

For A and v, (A^H*A)·v = 0 iff A^H·v = 0.

Русский

Для матрицы A и вектора v: (A^H A)·v = 0 эквивалентно A^H·v = 0.

LaTeX

$$(A^{\!H}A)\,v = 0 \iff A^{\!H}\,v = 0$$

Lean4

theorem conjTranspose_mul_self_mulVec_eq_zero (A : Matrix m n R) (v : n → R) : (Aᴴ * A) *ᵥ v = 0 ↔ A *ᵥ v = 0 := by
  simpa only [← Matrix.replicateCol_mulVec, replicateCol_eq_zero] using
    conjTranspose_mul_self_mul_eq_zero A (replicateCol (Fin 1) v)

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