This is a UW community formalization project centered on formalizing regular local rings.

Goal 1: Prove the undone theorems in EmdDim.lean.

Goal 2: Regular local rings are integral domains.

Goal 3: Regular local rings are Cohen Macaulay.

Goal 4: 1 dimensional Regular local rings are PIDs.