Is anyone working on Kaplansky's theorem?

Stream: new members

[Emilie Uthaiwat]

Hello everyone,

I am currently learning about Lean and trying to code Kaplansky's theorem for UFDs. Is anyone already working on it?

[Johan Commelin]

Welcome! :wave:
There was some discussion recently in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Descartes.20Rule.20of.20Signs

[Yaël Dillies]

Salut ! Long time no see :smiling_face:

[Riccardo Brasca]

@Emilie Uthaiwat is the student I am working with, and it seems nobody else is working on it. I've also realized that it can be used to prove that the localization of a UFD is a UFD (something I don't think it is mathlib).