Zulip Chat Archive

Stream: maths

Topic: field iff all ideals are trivial


view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 08:34):

I see in ring_theory/ideals/basic that all ideals in a field are trivial (i. e. the only ideals are 0 and the whole ring), that in a field the only prime ideal is 0 and that 0 is maximal. All these statements (provided that the ring is non-trivial) caracterise fields, so these three statements could be upgraded to "if-and-only-if" statements. Is it advisable to do so?

view this post on Zulip Johan Commelin (Nov 13 2020 at 08:37):

I didn't look at the current statements, but I guess that the assume [field K] as a typeclass argument. You loose that if you rephrase it using \iff.

view this post on Zulip Johan Commelin (Nov 13 2020 at 08:38):

So I would suggest writing seperate lemmas for the other direction field_of_ideal_eq_bot_or_top that can be used to construct a field instance.

view this post on Zulip Eric Wieser (Nov 13 2020 at 08:44):

Are you talking about things like docs#ideal.quotient.maximal_ideal_iff_is_field_quotient which are already iffs?

view this post on Zulip Filippo A. E. Nuccio (Nov 13 2020 at 09:04):

Ok, thanks. I will use that lemma.


Last updated: May 19 2021 at 02:10 UTC