exists_mulVec_eq_zero_iff — Mathlib

English

Relation between vecMul and determinant: a matrix M over a field has a nontrivial vector v with M v = 0 exactly when det M = 0.

Русский

Связь между vecMul и детерминантом: существует ненулевой вектор v с M v = 0 тогда и только тогда, когда det M = 0.

LaTeX

$$$\\exists v \\neq 0, M \\cdot v = 0 \\iff \\det M = 0$$$

Lean4

theorem exists_mulVec_eq_zero_iff {A : Type*} [DecidableEq n] [CommRing A] [IsDomain A] {M : Matrix n n A} :
    (∃ v ≠ 0, M *ᵥ v = 0) ↔ M.det = 0 :=
  exists_mulVec_eq_zero_iff' (FractionRing A)

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