Commit 2022-07-15 20:48 7929a63e
View on Github →feat(set_theory/zfc): more quotient lemmas (#15324)
It seems like we decided to use a custom mk definition for Set instead of quotient.mk. As such, we transfer the basic results on quotients to Set, in order to aid rewriting.