Sum of elements in a finite set

Stream: new members

[Manoj Kummini]

I have a polynomial ring and would like to take the sum and the product of some of the variables. This is what I tried; I have added the errors I got as comments.

import data.mv_polynomial.basic
import data.mv_polynomial.comm_ring
import data.zmod.basic
import ring_theory.ideal.operations


open mv_polynomial
noncomputable theory

section
-- column sum of an nxn matrix of variables  using zmod

parameter n : ℕ

abbreviation S := mv_polynomial (zmod n × zmod n) (zmod 101)
#check S
-- OK.

def h : zmod n → S := λ i, ∑ j in zmod n, X (i,j)
-- unexpected token at ∑
#check h
-- unknown identifier "h"

end

How should I do this? (I looked in Theorem proving in Lean and Mathematics in Lean for examples of using $\Sigma$ and $\prod$, but, I might have missed it.)

As a supplementary question: is there a way to search using these unicode characters (in zulip or in the archive on github)?
Thanks.

[Eric Wieser]

open_locale big_operators will enable that notation

[Eric Wieser]

The docs above docs#finset.sum should describe that notation

[Manoj Kummini]

Thanks.