English
If supports of p and q are disjoint, then the coefficients of p + q are exactly the union of the coefficient sets of p and q.
Русский
При непересечённых опорах p и q коэффициентов у p+q ровно объединение коэффициентов p и q.
LaTeX
$$$ \\text{If } \\mathrm{Supp}(p) \\cap \\mathrm{Supp}(q) = \\varnothing, \\ (p+q).\\mathrm{coeffs} = p.\\mathrm{coeffs} \\cup q.\\mathrm{coeffs}. $$$
Lean4
theorem coeffs_add [DecidableEq R] {p q : MvPolynomial σ R} (h : Disjoint p.support q.support) :
(p + q).coeffs = p.coeffs ∪ q.coeffs := by
ext r
simp only [mem_coeffs_iff, mem_support_iff, coeff_add, ne_eq, Finset.mem_union]
have hl (n : σ →₀ ℕ) (hne : p.coeff n ≠ 0) : q.coeff n = 0 :=
notMem_support_iff.mp <| h.notMem_of_mem_left_finset (mem_support_iff.mpr hne)
have hr (n : σ →₀ ℕ) (hne : q.coeff n ≠ 0) : p.coeff n = 0 :=
notMem_support_iff.mp <| h.notMem_of_mem_right_finset (mem_support_iff.mpr hne)
have hor (n) (h : ¬coeff n p + coeff n q = 0) : coeff n p ≠ 0 ∨ coeff n q ≠ 0 := by
by_cases hp : coeff n p = 0 <;> simp_all
refine ⟨fun ⟨n, hn1, hn2⟩ ↦ ?_, ?_⟩
· obtain (h | h) := hor n hn1
· exact Or.inl ⟨n, by simp [h, hn2, hl n h]⟩
· exact Or.inr ⟨n, by simp [h, hn2, hr n h]⟩
· rintro (⟨n, hn, rfl⟩ | ⟨n, hn, rfl⟩)
· exact ⟨n, by simp [hl n hn, hn]⟩
· exact ⟨n, by simp [hr n hn, hn]⟩
