Non Euclidean PID

A proof that $R = \mathbb{Z}[(1+i\sqrt{19})/2]$ is a PID but not a Euclidean domain, written in Lean 4

RoadMap

• Proving that a Euclidean Domain always has a universal side divisor
• Proving that having a Dedekind-Hasse norm implies being a Principal Ideal Domain
• Proving that $R$ is an integral domain
• Proving that $R$ has a Dedekind-Hasse norm
• Proving that $R$ has no universal side divisor