Polynomial GCD

Stream: new members

[Michael Levenkov]

I'm doing some work with polynomials and I'm having trouble with taking the GCD of two polynomials (MWE below).

import ring_theory.polynomial.basic
variables (R : Type) [comm_ring R]
def gcd_test (A B : polynomial R) := gcd A B

This gives the error

failed to synthesize type class instance for
R : Type,
_inst_1 : comm_ring R,
A B : polynomial R
⊢ cancel_comm_monoid_with_zero (polynomial R)

What am I missing here?

[Alex J. Best]

What does it mean to take the gcd of two polynomials over an arbitrary ring? If the base ring isn't a UFD then the polynomial ring won't be (citation needed..)

[Eric Wieser]

Adding [is_domain R] would fix your current error, but I think Alex is right

[Alex J. Best]

The definition of the gcd monoid structure on polynomial is at docs#polynomial.normalized_gcd_monoid, so you need to import ring_theory.polynomial.content and copy the assumptions there. Probably field R is sufficient too

[Alex J. Best]

Oh you need open_locale classical too if you just want to "do maths"

import ring_theory.polynomial.content
.
-- variables (R : Type) [comm_ring R] [is_domain R] [normalized_gcd_monoid R] -- or
variables (R : Type) [field R]
open_locale classical
noncomputable theory
def gcd_test (A B : polynomial R) := gcd A B