Regular local ring is a UFD project

Stream: general

[Leo Mayer]

I am working with a group at University of Washington's Math AI Lab to formalize the fact that a regular local ring is a UFD. The ultimate goal is to PR to Mathlib when we are finished. A few dependencies aren't yet in Mathlib, specifically @Nailin Guan and @Yongle Hu's work on the Auslander-Buchsbaum-Serre criterion https://github.com/leanprover-community/mathlib4/pull/29802, and @Riccardo Brasca's work on Kaplanski's criterion for being a UFD https://github.com/riccardobrasca/kaplanski4.

Are there plans for keep making progress with the Mathlib PR? What's the best way to proceed with our project in the meantime?

[Junyan Xu]

Kaplansky's criterion is in mathlib: UniqueFactorizationMonoid.iff_exists_prime_mem_of_isPrime