Commit 2024-03-17 09:55 6e3842d1

View on Github →

fix(Equiv/TransferInstance): Module instance diamond (#11419) Currently Equiv.algebra is defined in terms of RingHom.toAlgebra' which causes the induced Module R instance to not be defeq to the one from Equiv.module. This commit fixes this by defining Equiv.algebra in terms of Algebra.ofModule.

Estimated changes