vecMul_conjTranspose_mul_self_eq_zero

English

For any v, vecMul v (A^H A) = 0 iff vecMul v A^H = 0.

Русский

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

LaTeX

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

Lean4

theorem vecMul_conjTranspose_mul_self_eq_zero (A : Matrix m n R) (v : n → R) : v ᵥ* (Aᴴ * A) = 0 ↔ v ᵥ* Aᴴ = 0 := by
  simpa only [← Matrix.replicateRow_vecMul, replicateRow_eq_zero] using
    mul_conjTranspose_mul_self_eq_zero A (replicateRow (Fin 1) v)

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