mathlib

80d3ed8f - fix(algebra/euclidean_domain): remove decidable_eq assumption (#2362)

fix(algebra/euclidean_domain): remove decidable_eq assumption (#2362) This PR removes the `decidable_eq` assumption on the `field.to_euclidean_domain` instance. Decidable equality was only used to define the remainder with an if-then-else, but this can also be done by exploiting the fact that `0⁻¹ = 0`. The current instance is a bit problematic since it can cause `a + b : ℝ` to be noncomputable if type-class inference happens to choose the wrong instance (going through `euclidean_domain` instead of "directly" through some kind of ring).