Commit 2025-05-02 14:15 2142f9f5
View on Github →fix(Module/Equiv): fix LinearEquiv.coe_mk (#24553)
Make it work with any application of LinearEquiv.mk,
not only applications that go all the way to AddHom.mk.
Golf some of the proofs broken by this change.