English
For a semiring R, with k ≠ m and x ≠ 0, y ≠ 0 in R, the support of C x X^k + C y X^m is exactly {k, m}. Here C a denotes the constant polynomial with value a.
Русский
Для полиномиального кольца над полусоединенным кольцом R при k ≠ m и x ≠ 0, y ≠ 0 выполнено: опора полинома C x X^k + C y X^m равна {k, m}. Здесь C a означает константный полином со значением a.
LaTeX
$$$$\operatorname{Supp}(C x X^k + C y X^m) = \{k, m\}$$$$
Lean4
theorem support_binomial {k m : ℕ} (hkm : k ≠ m) {x y : R} (hx : x ≠ 0) (hy : y ≠ 0) :
support (C x * X ^ k + C y * X ^ m) = { k, m } :=
by
apply subset_antisymm (support_binomial' k m x y)
simp_rw [insert_subset_iff, singleton_subset_iff, mem_support_iff, coeff_add, coeff_C_mul, coeff_X_pow_self, mul_one,
coeff_X_pow, if_neg hkm, if_neg hkm.symm, mul_zero, zero_add, add_zero, Ne, hx, hy, not_false_eq_true, and_true]
