Zulip Chat Archive

Stream: Is there code for X?

Topic: Krull's Theorem


view this post on Zulip Kenji Nakagawa (Aug 16 2020 at 16:31):

More specifically, given any nonzero ring, there exists a maximal ideal.

This seems to be a relatively straightforward application of Zorn's lemma, so I was wondering if someone has already done it or wants to do so.

view this post on Zulip Markus Himmel (Aug 16 2020 at 16:33):

docs#ideal.exists_le_maximal

view this post on Zulip Bryan Gin-ge Chen (Aug 16 2020 at 16:34):

I guess that should get a docstring so that it's easier to find.

view this post on Zulip Markus Himmel (Aug 16 2020 at 17:03):

#3831

view this post on Zulip Bryan Gin-ge Chen (Aug 16 2020 at 17:17):

Thank you!


Last updated: May 07 2021 at 23:11 UTC