Commit 2024-10-18 13:37 e84469bd
View on Github →chore: do not use · ≈ · in Quotient.eq (#17594)
When Setoid is not an instance, we obviously want to avoid using · ≈ ·. Currently mathlib replicates the API around Quotient.mk for Quotient.mk'', but this is not needed because Quotient.mk doesn't use instance parameters now. After adjusting the API we can stop using Quotient.mk''.