mathlib3

feat(ring_theory/ideals): make ideal.quotient.field a discrete_field

#777

Merged