Commit 2026-03-23 12:20 26d69a00

View on Github →

chore: golf Ordinal.cof_univ (#36925) And tweak some existing theorems on univ.

Estimated changes

Modified Mathlib/SetTheory/Cardinal/Aleph.lean

deleted theorem Cardinal.type_cardinal

added theorem Ordinal.type_lt_cardinal

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

modified theorem Ordinal.cof_univ

Modified Mathlib/SetTheory/Ordinal/Basic.lean

added theorem Ordinal.type_lt_ordinal