Zulip Chat Archive
Stream: mathlib4
Topic: DFinsupp.instEquivLikeLinearEquiv
Wrenna Robson (Jun 20 2025 at 15:24):
Why does DFinsupp.instEquivLikeLinearEquiv exist? Is it not identical to LinearEquiv.instEquivLike? What am I missing?
Yaël Dillies (Jun 20 2025 at 16:10):
docs#DFinsupp.instEquivLikeLinearEquiv
Yaël Dillies (Jun 20 2025 at 16:10):
Looks duplicated, yes
Last updated: Dec 20 2025 at 21:32 UTC