σ : Type u_1
R : Type u_2
τ : Type ?u.91991
S : Type ?u.91994
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ esymm σ R n = ∑ x in powersetLen n univ, ∏ x in x, ↑(monomial (Finsupp.single x 1)) 1
σ : Type u_1
R : Type u_2
τ : Type ?u.91991
S : Type ?u.91994
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ esymm σ R n = ∑ t in powersetLen n univ, ↑(monomial (∑ i in t, Finsupp.single i 1)) 1
simp_rw [monomial_sum_one]
no goals
σ : Type u_1
R : Type u_2
τ : Type ?u.91991
S : Type ?u.91994
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
n : ℕ
⊢ esymm σ R n = ∑ x in powersetLen n univ, ∏ x in x, ↑(monomial (Finsupp.single x 1)) 1
rfl