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
.