polynomial ring over a field

Stream: new members

[Jack J Garzella]

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]

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]

import ring_theory.principal_ideal_domain
import data.polynomial

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

[Reid Barton]

Or by apply_instance I imagine?

[sha monad]

(deleted)

[Jack J Garzella]

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

[Sayantan Santra]

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

[Patrick Massot]

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]

Patrick Massot Thank you.