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