English
For any c: σ → K, the indicator polynomial indicator(c) lies in the subspace restrictDegree(σ, K, |K| − 1), i.e. its per-variable degree is bounded by card(K) − 1.
Русский
Для любого отображения c: σ → K индикатор-indicator(c) принадлежит подпространству restrictDegree(σ, K, |K| − 1), то есть для каждой переменной показатель степени ограничен величиной card(K) − 1.
LaTeX
$$$\\\\mathrm{indicator}(c) \\\\in \\\\mathrm{restrictDegree}(\\\\sigma, K, |K| - 1)$$$$
Lean4
theorem indicator_mem_restrictDegree (c : σ → K) : indicator c ∈ restrictDegree σ K (Fintype.card K - 1) := by
classical
rw [mem_restrictDegree_iff_sup, indicator]
intro n
refine le_trans (Multiset.count_le_of_le _ <| degrees_indicator _) (le_of_eq ?_)
simp_rw [← Multiset.coe_countAddMonoidHom, map_sum, AddMonoidHom.map_nsmul, Multiset.coe_countAddMonoidHom,
nsmul_eq_mul, Nat.cast_id]
trans
· refine Finset.sum_eq_single n ?_ ?_
· intro b _ ne
simp [Multiset.count_singleton, ne, if_neg (Ne.symm _)]
· intro h; exact (h <| Finset.mem_univ _).elim
· rw [Multiset.count_singleton_self, mul_one]
