Zulip Chat Archive

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 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

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?

sha monad (May 06 2020 at 03:36):


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

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

Sayantan Santra (Jun 16 2023 at 04:23):

Hi, is this ported to Mathlib4 yet? I was unable to find anything similar to this.

Patrick Massot (Jun 16 2023 at 04:33):

The type class system knows about all this

import Mathlib.Data.Polynomial.FieldDivision

example {F : Type} [Field F] : IsPrincipalIdealRing (Polynomial F) :=
by infer_instance

example {F : Type} [Field F] : IsDomain (Polynomial F) := by infer_instance

Sayantan Santra (Jun 16 2023 at 04:35):

Patrick Massot Thank you.

Last updated: Dec 20 2023 at 11:08 UTC