Krull's Theorem

Stream: Is there code for X?

[Kenji Nakagawa]

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.

[Markus Himmel]

docs#ideal.exists_le_maximal

[Bryan Gin-ge Chen]

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

[Markus Himmel]

#3831

[Bryan Gin-ge Chen]

Thank you!