field iff all ideals are trivial

Stream: maths

[Filippo A. E. Nuccio]

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?

[Johan Commelin]

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.

[Johan Commelin]

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.

[Eric Wieser]

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

[Filippo A. E. Nuccio]

Ok, thanks. I will use that lemma.