Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 23:41 e09e8770

View on Github →

refactor(set_theory/cardinal/cofinality): infer arguments (#14251) We make one of the arguments in cof_type_le and lt_cof_type implicit.

Estimated changes

modified theorem ordinal.cof_type_le
modified theorem ordinal.lt_cof_type