# Zulip Chat Archive

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

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

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