root_ne_neg_of_ne — Mathlib

English

If i ≠ j are distinct roots in the base b, then P.root i ≠ −P.root j.

Русский

Если i ≠ j — корни базиса b, то P.root i ≠ −P.root j.

LaTeX

$$$\\text{If } i,j\\in b.support,\\ i\\neq j, \\text{ then } P.root(i) \\neq -P.root(j).$$$

Lean4

theorem root_ne_neg_of_ne [Nontrivial R] {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) (hij : i ≠ j) :
    P.root i ≠ -P.root j := by
  classical
  intro contra
  have :=
    linearIndepOn_iff'.mp b.linearIndepOn_root ({ i, j } : Finset ι) 1 (by simp [Set.insert_subset_iff, hi, hj])
      (by simp [Finset.sum_pair hij, contra])
  simp_all

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