mathlib3

d2b18a18 - feat(algebra/field, ring_theory/ideal/basic): an ideal is maximal iff the quotient is a field (#3986)

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. Co-authored-by: AlexandruBosinta <32337238+AlexandruBosinta@users.noreply.github.com>