## Stream: new members

### Topic: polynomial ring over a field

#### Jack J Garzella (May 05 2020 at 03:27):

Does mathlib have the following theorem?

Given a field $F$, the polynomial ring $F[X]$ is a PID.

I think this should be in mathlib, it seems very basic compared to some of the things that are in there, but I can't find it in polynomial.lean or principal_ideal_domain.lean

#### Alex J. Best (May 05 2020 at 03:30):

There is https://leanprover-community.github.io/mathlib_docs/data/polynomial.html#polynomial.euclidean_domain and then also euclidean_domain.to_principal_ideal_domain

#### Scott Morrison (May 05 2020 at 23:38):

import ring_theory.principal_ideal_domain
import data.polynomial

example {F : Type} [field F] : principal_ideal_domain (polynomial F) :=
by library_search


#### Reid Barton (May 05 2020 at 23:42):

Or by apply_instance I imagine?

(deleted)

#### Jack J Garzella (May 07 2020 at 00:08):

by apply_instance doesn't seem to work, but library_search does the trick

Last updated: May 14 2021 at 13:24 UTC