linearIndependent_iff — Mathlib

English

If i and j are such that P.root i + P.root j lies in the range of P.root, then [P.root i, P.root j] are linearly independent.

Русский

Если i и j таковы, что P.root i + P.root j лежит в образе P.root, то векторная пара {P.root i, P.root j} линейно независима.

LaTeX

$$$$ (P.root i + P.root j) \\in \\operatorname{range}(P.root) \\Rightarrow \\operatorname{LI}_R(\\![P.root i, P.root j]\\!). $$$$

Lean4

theorem linearIndependent_iff [Nontrivial R] [P.IsReduced] :
    LinearIndependent R ![P.root i, P.root j] ↔ i ≠ j ∧ P.root i ≠ -P.root j :=
  by
  refine ⟨fun h ↦ ?_, fun ⟨h, h'⟩ ↦ linearIndependent P h h'⟩
  rw [LinearIndependent.pair_iff] at h
  contrapose! h
  rcases eq_or_ne i j with rfl | h'
  · exact ⟨1, -1, by simp⟩
  · rw [h h']
    exact ⟨1, 1, by simp⟩

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