Commit 2021-05-12 15:10 08f44043
View on Github →refactor(ring_theory/perfection): remove coercion in the definition of the type (#7583)
Defining the type ring.perfection R p as a plain subtype (but inheriting the semiring or ring instances from a subsemiring structure) removes several coercions and helps Lean a lot when elaborating or unifying.