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.