Commit 2026-03-30 08:57 e1df0077

View on Github →

feat: bundled version of Cardinal.ord_eq (#36928) For any type, there exists a (bundled) well-ordering whose order type is ord #α.

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib/FieldTheory/CardinalEmb.lean

Modified Mathlib/SetTheory/Cardinal/Cofinality.lean

Modified Mathlib/SetTheory/Cardinal/Regular.lean

Modified Mathlib/SetTheory/Ordinal/Basic.lean

modified theorem Cardinal.card_typein_lt

added theorem Cardinal.exists_ord_eq_type_lt

added theorem Cardinal.mk_Iio_lt

deleted theorem Cardinal.mk_Iio_ord_toType

added theorem Cardinal.mk_Iio_toType_ord_lt