English
In a nontrivial commutative ring with nontrivial index, for any a ∈ m → α there exists b ≠ 0 such that dotProduct b a = 0.
Русский
В ненулевой коммутативной кольцевой системе с ненуловым индексом для любого a ∈ m → α существует b ≠ 0 такое, что dotProduct(b,a) = 0.
LaTeX
$$$\exists b \ne 0, \ dotProduct(b,a) = 0$$$
Lean4
/-- 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. -/
theorem exists_ne_zero_dotProduct_eq_zero (a : m → α) : ∃ b ≠ 0, b ⬝ᵥ a = 0 :=
by
obtain ⟨i, j, hij⟩ : ∃ i j : m, i ≠ j := nontrivial_iff.mp ‹_›
classical
use
if a i = 0 then Pi.single i 1
else if a j = 0 then Pi.single j 1 else fun k => if k = i then a j else if k = j then -a i else 0
split_ifs with h h2
· simp [h]
· simp [h2]
· refine ⟨Function.ne_iff.mpr ⟨i, by simp [h2]⟩, ?_⟩
simp [dotProduct, Finset.sum_ite, Finset.sum_eq_ite i, hij.symm, mul_comm (a i)]
