linearIndependent_of_sub_mem_range_root

English

If i and j satisfy that P.root i - P.root j lies in the range of P.root, then {P.root i, P.root j} is linearly independent.

Русский

Если P.root i - P.root j ∈ range(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_of_sub_mem_range_root [CharZero R] [NoZeroSMulDivisors ℤ M] [P.IsReduced] {i j : ι}
    (h : P.root i - P.root j ∈ range P.root) : LinearIndependent R ![P.root i, P.root j] :=
  by
  suffices LinearIndependent R ![P.root i, P.root (P.reflectionPerm j j)] by simpa using this
  apply P.linearIndependent_of_add_mem_range_root
  simpa [sub_eq_add_neg] using h

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