Commit 2026-04-13 10:18 4bd98997
View on Github →refactor(Algebra): replace RingEquivClass.toRingEquiv by structure-specific coercions (#21031)
Remove the coercion from E to RingEquiv assuming RingEquivClass E and given by RingEquivClass.toRingEquiv. For each concrete type, reimplement this coercion through the relevant structure projection.