Type mismatch/failed to synthesize

Stream: new members

[Pim Otte]

In the following definition, I'm getting an error because it failed to synthesize type class instance and there's a type mismatch.

I'm trying to express that a waring decomposition is a way to write a polynomial as sum of powers of linear forms. The issue, I think, is that you can't raise a power in the submodule. What I think I want is to coerce i.2 into a polynomial in the bigger ring and I think that addresses both issues. If yes, how would I go about that? If no, what should I be looking at?

import data.mv_polynomial.basic
import ring_theory.polynomial.homogeneous

open_locale big_operators

def is_waring_decomposition {σ : Type*} {R : Type*} [comm_semiring R] (p : mv_polynomial σ R) (s : finset (ℕ × mv_polynomial.homogeneous_submodule σ R 1)) := (∑ i in s, i.2^i.1) = p