Zulip Chat Archive

Stream: new members

Topic: polynomial ring over a field


view this post on Zulip Jack J Garzella (May 05 2020 at 03:27):

Does mathlib have the following theorem?

Given a field F F , the polynomial ring F[X] 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (May 05 2020 at 23:42):

Or by apply_instance I imagine?

view this post on Zulip sha monad (May 06 2020 at 03:36):

(deleted)

view this post on Zulip 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