Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-14 17:04 6cdc30d7

View on Github →

golf(set_theory/ordinal/basic): golf theorems on cardinal.ord and ordinal.card (#14709)

Estimated changes

modified theorem cardinal.mk_ord_out