exists_vecMul_eq_zero_iff — Mathlib

English

The transpose version: there exists a nonzero v with v^T M = 0 if and only if det M = 0.

Русский

Версия транспонирования: существует ненулевой вектор v такой, что v^T M = 0 тогда и только тогда, когда det M = 0.

LaTeX

$$$\\exists v \\neq 0, v^T M = 0 \\iff \\det M = 0\$$$

Lean4

theorem exists_vecMul_eq_zero_iff {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
    (∃ v ≠ 0, v ᵥ* M = 0) ↔ M.det = 0 := by
  simpa only [← M.det_transpose, ← mulVec_transpose] using exists_mulVec_eq_zero_iff

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