Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-22 15:58 87ea7806

View on Github →

chore(set_theory/cardinal): use protected instead of private (#9869) Also use mk_congr.

Estimated changes

modified theorem cardinal.mk_emptyc