Theorems · Theorem · linear algebra

Matrix.nondegenerate_def

∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Fintype m]
  [inst_2 : Fintype n],
  M.Nondegenerate ↔
    (∀ (v : m → R), (∀ (w : n → R), v ⬝ᵥ M.mulVec w = 0) → v = 0) ∧
      ∀ (w : n → R), (∀ (v : m → R), v ⬝ᵥ M.mulVec w = 0) → w = 0

Defined in

Mathlib.LinearAlgebra.Matrix.Nondegenerate

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommSemiringFintypeFintype