Theorems · Theorem · linear algebra

Matrix.det_eq_zero_of_mulVec_eq_zero_of_mem_nonZeroDivisors

∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] {M : Matrix n n α}
  {v : n → α}, M.mulVec v = 0 → ∀ {i : n}, v i ∈ nonZeroDivisors α → M.det = 0

Defined in

Mathlib.LinearAlgebra.Matrix.Adjugate

Cited by

0 results in Mathlib

Foundations

Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeCommRing