Theorems · Theorem · linear algebra

exists_ne_zero_dotProduct_eq_zero

∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α),
  ∃ b, b ≠ 0 ∧ b ⬝ᵥ a = 0

For any vector a in a nontrivial commutative ring with nontrivial index, there exists a non-zero vector b such that b ⬝ᵥ a = 0. In other words, there exists a non-zero orthogonal vector.

Defined in

Mathlib.Data.Matrix.Mul

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeCommRingNontrivialNontrivial