linearIndependent_pair_of_ne — Mathlib

English

If i ≠ j in the base b, then the two roots P.root i and P.root j are linearly independent (as a 2-vector).

Русский

Если i ≠ j в базе b, то корни P.root i и P.root j линейно независимы (как два вектора).

LaTeX

$$$\\text{If } i\\neq j, \\text{ then } \\ linearIndependent_R( ![P.root i, P.root j] ).$$$

Lean4

theorem linearIndependent_pair_of_ne {i j : b.support} (hij : i ≠ j) : LinearIndependent R ![P.root i, P.root j] :=
  by
  have : ({(j : ι), (i : ι)} : Set ι) ⊆ b.support := by simp [pair_subset_iff]
  rw [← linearIndepOn_id_range_iff (by aesop)]
  simpa [image_pair] using LinearIndepOn.id_image <| b.linearIndepOn_root.mono this

Похожие утверждения