English
Let K be a finite ring and σ a finite set. For every function c: σ → K, the multidegree (degrees) of the indicator polynomial ind(c) is bounded by the sum over s ∈ σ of (|K| − 1) times the unit exponent at s, i.e. deg(indicator(c)) ≤ ∑_{s∈σ} (|K|−1) • e_s.
Русский
Пусть K — конечное кольцо, σ — конечное множество. Для любой функции c: σ → K, множество степеней индикаторного многочлена ind(c) ограничено сверху суммой по s∈σ от (|K|−1) умноженного на единичный вектор степени в координате s: deg(indicator(c)) ≤ ∑_{s∈σ} (|K|−1) • e_s.
LaTeX
$$$\\\\mathrm{degrees}(\\\\mathrm{indicator}(c)) \\\\le \\\\sum_{s \\\\in \\\\sigma} (|K| - 1) \\\\cdot \\\\{s\\\\}$$
Lean4
theorem degrees_indicator (c : σ → K) : degrees (indicator c) ≤ ∑ s : σ, (Fintype.card K - 1) • { s } :=
by
rw [indicator]
classical
refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
rw [degrees_one, Multiset.zero_union]
refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
refine degrees_sub_le.trans ?_
rw [degrees_C, Multiset.union_zero]
exact degrees_X' _
