Commit 2020-08-31 15:32 d2b18a18

feat(algebra/field, ring_theory/ideal/basic): an ideal is maximal iff the quotient is a field (#3986) One half of the theorem was already proven (the implication maximal ideal implies that the quotient is a field), but the other half was not, mainly because it was missing a necessary predicate. I added the predicate is_field that can be used to tell Lean that the usual ring structure on the quotient extends to a field. The predicate along with proofs to move between is_field and field were provided by Kevin Buzzard. I also added a lemma that the inverse is unique in is_field. At the end I also added the iff statement of the theorem.