Zulip Chat Archive

Stream: mathlib4

Topic: Equiv.Set.ofEq

Violeta Hernández (Jan 04 2025 at 09:30):

We have both docs#Equiv.Set.ofEq and docs#Equiv.setCongr. Which one should stay and which one should go?

Violeta Hernández (Jan 04 2025 at 09:30):

Note that we have docs#OrderIso.setCongr but not docs#OrderIso.ofEq (which is how I noticed this issue to begin with)

Kevin Buzzard (Jan 04 2025 at 09:33):

(deleted)

Violeta Hernández (Jan 04 2025 at 09:34):

Oops, missing namespace

Last updated: May 02 2025 at 03:31 UTC