defining polynomials inside a polynomial ring.

Stream: new members

[Manoj Kummini]

I would like to define a polynomial ring $K[X_0, \ldots, X_{2n-1}]$ and polynomials $X_iX_{i+n}, 0 \le i \le n-1$. I tried the following:

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

parameter n : ℕ
abbreviation R := mv_polynomial (fin (2*n)) (zmod 101)
#check R

def f : (fin (2*n)) → R := λ i, (X i)*(X (i+n))
abbreviation f : (fin (2*n)) → R := λ i, (X i)*(X (i+n))
-- type mismatch at application
--  i + n
-- term
--  n
-- has type
--  ℕ
-- but is expected to have type
--  fin (2 * n)

#check f
#check (f 0)
-- failed to synthesize type class instance for
-- n : ℕ
-- ⊢ has_zero (fin (2 * n))

How should I define these polynomials?

[Eric Wieser]

You'd do best to define the function fin (2*n) → fin (2*n) := λ i, i + n (which is the bit that is wrong right now) separately.

[Eric Wieser]

Is it possible you want zmod (2*n) instead? What's your intention when n=0?

[Eric Wieser]

eg

def dual_var (n : ℕ) : fin (2*n) ≃ fin (2*n) := (fin_rotate _)^n

[Manoj Kummini]

Eric Wieser said:

Is it possible you want zmod (2*n) instead? What's your intention when n=0?

Thanks; this worked. I won't need the case n=0. The proof I am trying to formalize is not an inductive proof.

[Eric Wieser]

You might even want to use bool × fin n instead of fin (2*n)

[Eric Wieser]

Or fin n ⊕ fin n, and use sum.swap instead of + n