English
For n terms with pairwise distinct exponents k_i and nonzero coefficients x_i, the polynomial ∑ i C(x_i) X^{k_i} has exactly n nonzero terms, i.e., its support has cardinality n.
Русский
Для суммы из n мономов с попарно различными степенями k_i и ненулевыми коэффициентами x_i, полином ∑ i C(x_i) X^{k_i} имеет ровно n ненулевых членов, т. е. опора полинома имеет кардинал ровно n.
LaTeX
$$$\\#\\left(\\sum_i C(x_i) X^{k_i}\\right).\\text{support} = n$$$
Lean4
theorem card_support_eq' {n : ℕ} (k : Fin n → ℕ) (x : Fin n → R) (hk : Function.Injective k) (hx : ∀ i, x i ≠ 0) :
#(∑ i, C (x i) * X ^ k i).support = n :=
by
suffices (∑ i, C (x i) * X ^ k i).support = image k univ by rw [this, univ.card_image_of_injective hk, card_fin]
simp_rw [Finset.ext_iff, mem_support_iff, finset_sum_coeff, coeff_C_mul_X_pow, mem_image, mem_univ, true_and]
refine fun i => ⟨fun h => ?_, ?_⟩
· obtain ⟨j, _, h⟩ := exists_ne_zero_of_sum_ne_zero h
exact ⟨j, (ite_ne_right_iff.mp h).1.symm⟩
· rintro ⟨j, _, rfl⟩
rw [sum_eq_single_of_mem j (mem_univ j), if_pos rfl]
· exact hx j
· exact fun m _ hmj => if_neg fun h => hmj.symm (hk h)
