Zulip Chat Archive

Stream: new members

Topic: Is anyone working on Kaplansky's theorem?


Emilie Uthaiwat (Jan 13 2023 at 15:45):

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 (Jan 13 2023 at 15:52):

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 (Jan 13 2023 at 15:57):

Salut ! Long time no see :smiling_face:

Riccardo Brasca (Jan 13 2023 at 16:11):

@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).


Last updated: Dec 20 2023 at 11:08 UTC