single universe in ring_theory.polynomial.vieta

Stream: new members

[María Inés de Frutos Fernández]

Why are the ring R and the indexing fintype σ required to live in the same universe in the file ring_theory.polynomial.vieta? Changing this does not seem to cause anything to break.
I am asking in particular because I would like to useprod_X_add_C_eval with σequal to fin n , regardless of the universe of definition of R (but I could use ulift (fin n) if necessary).

[Eric Rodriguez]

if it doesn't break anything, I'd think a PR generalising it would be totally welcome!

[María Inés de Frutos Fernández]

Ok, thanks! I'll PR the change.

[Yaël Dillies]

Yeah, you can literally replace Type u by Type* everywhere