no goals
σ : Type u_1
R : Type u_2
τ : Type ?u.96806
S : Type ?u.96809
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Fintype τ
⊢ esymm σ R 0 = 1
simp only [esymm, powersetLen_zero, sum_singleton, prod_empty]