Zulip Chat Archive

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[X0,,X2n1]K[X_0, \ldots, X_{2n-1}] and polynomials XiXi+n,0in1X_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