evaluating polynomials

Stream: new members

[Ralf Stephan]

Is it possible to evaluate a multivariate polynomial with coefficients in ZZ at QQ (i.e., substitute something from QQ in the variables)? My attempt:

import Mathlib
set_option autoImplicit false
open MvPolynomial

example (k n : ℕ) (a : Fin 3 → ℚ) (ha : a = fun (i : Fin 3) ↦ (1 : ℚ) / i) :
    ∃ P : MvPolynomial (Fin 3) ℤ, eval a P = 0 := by sorry

application type mismatch
  (eval a) P
argument
  P
has type
  MvPolynomial (Fin 3) ℤ : Type
but is expected to have type
  MvPolynomial (Fin 3) ℚ : Type

[Ruben Van de Velde]

Does MvPolynomial have aeval?

[Ralf Stephan]

Yes, and I ignored it.

[Ralf Stephan]

I will add something to the preamble of Algebra/MvPolynomial/Basic.

[Ralf Stephan]

Thanks!