Commit 2026-06-21 21:14 7a1a9e04
View on Github →perf(Algebra/Algebra/Equiv): mark coe_ringEquiv with defeq again (#40873)
This PR reverts the proof of coe_ringEquiv back to := rfl after #40834, which apparently is necessary for performance reasons.