Zulip Chat Archive
Stream: mathlib4
Topic: Quotients are not reducibly defeq to their definitions
Notification Bot (Feb 04 2025 at 14:11):
This topic was moved to #lean4 > instances don't apply to instance-defeq types by Johan Commelin.
Last updated: May 02 2025 at 03:31 UTC