IsPrincipalIdealRing ℤ

Stream: Is there code for X?

[Antoine Chambert-Loir]

I had a problem with shake in #23710.
What is the standard import to choose so that mathlib is aware that ℤ is a principal ideal domain?
The instance I ended getting passed through docs#EuclideanDomain.to_principal_ideal_domain, using docs#Int.euclideanDomain (which, mathematically, is sound, of course.)

[Yaël Dillies]

Mathlib.RingTheory.Int.Basic, I believe