Theorems · Theorem · linear algebra

Matrix.single_mul_single_of_ne

∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq l] [inst_1 : DecidableEq m]
  [inst_2 : DecidableEq n] [inst_3 : Fintype m] [inst_4 : NonUnitalNonAssocSemiring α] (c : α) (i : l) (j k : m)
  {l_1 : n}, j ≠ k → ∀ (d : α), Matrix.single i j c * Matrix.single k l_1 d = 0

Defined in

Mathlib.Data.Matrix.Basis

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEqDecidableEqFintypeNonUnitalNonAssocSemiring