Skip to content

README.md

Latest commit

 

History

History
11 lines (8 loc) · 444 Bytes

README.md

File metadata and controls

11 lines (8 loc) · 444 Bytes

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