## Stream: maths

### Topic: field iff all ideals are trivial

#### 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?

#### 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.

#### 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.