English
Let a be a finitely supported function a: σ →₀ ℕ, p a multivariate polynomial, and s a nonzero coefficient. If a does not appear in p, then the support of the monomial a with coefficient s is disjoint from the support of p.
Русский
Пусть a: σ →₀ ℕ имеет конечную опору, p — многочлен по переменным σ над кольцом R, и s ≠ 0. Если a не входит в опору p, то опоры моноюма с коэффициентом s и p — попарно не имеют общих элементов.
LaTeX
$$$(a \notin p.\mathrm{support}) \rightarrow (s \neq 0) \rightarrow \mathrm{Disjoint}((\mathrm{monomial}\;a\;s).\mathrm{support},\ p.\mathrm{support})$$$
Lean4
theorem disjoint_support_monomial {a : σ →₀ ℕ} {p : MvPolynomial σ R} {s : R} (ha : a ∉ p.support) (hs : s ≠ 0) :
Disjoint (monomial a s).support p.support := by
classical simpa [support_monomial, hs] using notMem_support_iff.mp ha
