English
For i, j in the support of b with i ≠ j, the difference P.root(i) - P.root(j) does not belong to the range of P.root.
Русский
Для i, j в поддержке b, при i ≠ j разность P.root(i) - P.root(j) не принадлежит диапазону P.root.
LaTeX
$$P.root i - P.root j ∉ range P.root$$
Lean4
theorem sub_notMem_range_root {i j : ι} (hi : i ∈ b.support) (hj : j ∈ b.support) :
P.root i - P.root j ∉ range P.root := by
rcases eq_or_ne j i with rfl | hij
· simpa only [sub_self, mem_range, not_exists] using fun k ↦ P.ne_zero k
classical
let f : ι → ℤ := fun k ↦ if k = i then 1 else if k = j then -1 else 0
have hf : ∑ k ∈ b.support, f k • P.root k = P.root i - P.root j :=
by
have : { i, j } ⊆ b.support := by aesop (add simp Finset.insert_subset_iff)
rw [← Finset.sum_subset (s₁ := { i, j }) (s₂ := b.support) (by aesop) (by aesop), Finset.sum_insert (by aesop),
Finset.sum_singleton]
simp [f, hij, sub_eq_add_neg]
intro contra
rcases b.pos_or_neg_of_sum_smul_root_mem f (by rwa [hf]) (by aesop) with pos | neg
· simpa [hij, f] using le_of_lt pos j
· simpa [hij, f] using le_of_lt neg i
