English
If 0 < n ≤ |σ|, then the degree set of esymm(σ,R,n) equals the full set of indices: esymm(σ,R,n).degrees = (univ : Finset σ).val.
Русский
При 0 < n ≤ |σ| множество степеней esymm(σ,R,n) равно всем индексам: esymm(σ,R,n).degrees = (univ).val.
LaTeX
$$$ (\\text{esymm}(\\sigma,R,n)).\\text{degrees} = (\\mathrm{univ} : Finset \\sigma).val \\quad \\text{при } 0 < n \\le |\\sigma|. $$$
Lean4
theorem degrees_esymm [Nontrivial R] {n : ℕ} (hpos : 0 < n) (hn : n ≤ Fintype.card σ) :
(esymm σ R n).degrees = (univ : Finset σ).val := by
classical
have : (Finsupp.toMultiset ∘ fun t : Finset σ => ∑ i ∈ t, Finsupp.single i 1) = val :=
by
funext
simp
rw [degrees_def, support_esymm, sup_image, this]
have : ((powersetCard n univ).sup (fun (x : Finset σ) => x)).val = sup (powersetCard n univ) val := by
refine comp_sup_eq_sup_comp _ ?_ ?_ <;> simp
rw [← this]
obtain ⟨k, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hpos.ne'
simpa using powersetCard_sup _ _ (Nat.lt_of_succ_le hn)
