finset.prod

Stream: new members

[Manoj Kummini]

I am trying to take the product along the rows and the columns of a matrix of variables. This is what I tried, but I get a type mismatch.

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


open mv_polynomial
open_locale big_operators
noncomputable theory

section
-- trying to work with a mxn matrix.

parameter m : ℕ
parameter n : ℕ
abbreviation rows := (finset.range m)
abbreviation cols := (finset.range n)

abbreviation R := mv_polynomial ( rows × cols ) (zmod 101)
#check R

def entries : rows → cols → R := λ i, λ j, X (i,j)
parameter i: rows
#check entries i

#check cols
#check cols.prod

def row_prod : rows → R := λ i, cols.prod  (entries i)
-- type mismatch at application
--   cols.prod (entries i)
-- term
--   entries i
-- has type
--   ↥cols → R
-- but is expected to have type
--   ℕ → R

end

Before using finset.range, I tried to use zmod and fin, both of which gave other type mismatches. I don't know if finset.range is the correct thing to use here, but I found some discussion in the archive where it is used in the context of Witt vectors.

section
-- To understand finset.sum

def p : zmod 4 → nat := λ i, i
def q := finset.sum (zmod 4) p
-- type mismatch at application
--   finset.sum (zmod 4)
-- term
--   zmod 4
-- has type
--   Type : Type 1
-- but is expected to have type
--   finset ?m_1 : Type ?

def p1 : (fin 4) → nat := λ i, i
def q1 := finset.sum (fin 4) p1
-- similar error as above.

-- finset.range
def p2 : nat → nat := λ i, i
def q2 := (finset.range 4).sum  p2

#check p
#check q

#check p1
#check q1
#check p2
#check q2
#reduce q2
-- 6
end

Thanks.

[Eric Wieser]

The canonical m x n matrix type is matrix (fin m) (fin n), but in principle your approach of using finset.range m should work.

[Alex J. Best]

A few comments:

• We generally recommend avoiding using parameters as they often confuse things more than they help, you might be better off just using variables.
• In mathlib there is already a type of matrices that is likely useful to you
• for rows and cols you should use the type fin n or fin m rather than finset.range which returns a list, this is then coerced into a type which adds those arrows everywhere

[Eric Wieser]

The arguments to docs#finset.sum do not match what you're passing. You want (finset.univ : finset (zmod 4)) in place of zmod 4

[Eric Wieser]

Or better, use the syntax for that ∑ i : zmod 4, p i

[Alex J. Best]

This hopefully does what you want:

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


open mv_polynomial
open_locale big_operators
noncomputable theory

section
-- trying to work with a mxn matrix.

parameter m : ℕ
parameter n : ℕ
abbreviation rows := (fin m)
abbreviation cols := (fin n)

abbreviation R := mv_polynomial ( rows × cols ) (zmod 101)
#print R

def entries : matrix rows cols R := λ i, λ j, X (i,j)
variable  i: rows
#check entries

#check cols

def row_prod (i : rows) : R := ∏ j, entries i j

#print row_prod

end
-- we can even do some "computation" to check everything makes sense


#simp [row_prod, entries, fin.prod_univ_succ] row_prod 2 2 1

[Manoj Kummini]

Thanks. This is what I am looking for. I did not understand what the last line is; couldn't find #simp in Mathematics in Lean and Theorem proving in Lean. Is it to run the simp tactic on some goal and print the result?

[Kyle Miller]

@Manoj Kummini I hadn't seen this before -- that's a cool command to have. Here's the documentation: https://leanprover-community.github.io/mathlib_docs/commands.html##simp

[Kyle Miller]

(I'd forgotten about #where... I was thinking recently about how nice it would be to be able to see the current namespace and variable declarations.)

[Manoj Kummini]

Kyle Miller said:

Manoj Kummini I hadn't seen this before -- that's a cool command to have. Here's the documentation: https://leanprover-community.github.io/mathlib_docs/commands.html##simp

Thank you.