Zulip Chat Archive
Stream: mathlib4
Topic: Duplicate instances of `Subsingleton (Fin _)`
Chris Wong (Feb 19 2025 at 03:17):
docs#Fin.subsingleton_zero
docs#Fin.subsingleton_one
docs#subsingleton_fin_zero
docs#subsingleton_fin_one
Should we delete the latter?
Kyle Miller (Feb 19 2025 at 03:46):
Yes, I think so.
Last updated: May 02 2025 at 03:31 UTC