conjTranspose_mul_self_eq_zero — Mathlib

English

Over a star-ordered ring with no zero divisors, A^H A = 0 implies A = 0; equivalently A ≠ 0 implies A^H A ≠ 0.

Русский

Для кольца со звёздочкой без делителей нуля, если A^H A = 0, то A = 0; иначе A ≠ 0 ⇒ A^H A ≠ 0.

LaTeX

$$$A^{\\mathrm{H}} A = 0 \\iff A = 0$$$

Lean4

@[simp]
theorem conjTranspose_mul_self_eq_zero {n} {A : Matrix m n R} : Aᴴ * A = 0 ↔ A = 0 :=
  ⟨fun h => Matrix.ext fun i j => (congr_fun <| dotProduct_star_self_eq_zero.1 <| Matrix.ext_iff.2 h j j) i, fun h =>
    h ▸ Matrix.mul_zero _⟩

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