## Stream: new members

### Topic: defining polynomials inside a polynomial ring.

#### Manoj Kummini (Jul 16 2021 at 16:24):

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 (Jul 16 2021 at 16:27):

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 (Jul 16 2021 at 16:28):

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

#### Eric Wieser (Jul 16 2021 at 16:32):

eg

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


#### Manoj Kummini (Jul 16 2021 at 17:25):

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 (Jul 16 2021 at 20:27):

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

#### Eric Wieser (Jul 16 2021 at 20:30):

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

Last updated: Dec 20 2023 at 11:08 UTC