linearIndependent_of_add_mem_range_root

English

If i, j are indices with P.root i + P.root j in the range of P.root, then {P.root i, P.root j} is linearly independent.

Русский

Если i, j удовлетворяют 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_add_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
  refine IsReduced.linearIndependent P (fun hij ↦ ?_) (fun hij ↦ P.zero_notMem_range_root ?_)
  · rw [hij, ← two_smul (R := ℕ)] at h
    exact P.nsmul_notMem_range_root h
  · rwa [hij, neg_add_cancel] at h

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