Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-11 13:55 380e28e9

View on Github →

chore(set_theory/ordinal_arithmetic): Golfed some proofs (#11369)

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

modified theorem ordinal.blsub_le_enum_ord

modified def ordinal.enum_ord.order_iso

modified theorem ordinal.enum_ord.strict_mono

modified theorem ordinal.enum_ord.surjective

modified def ordinal.enum_ord

modified theorem ordinal.enum_ord_mem

modified theorem ordinal.enum_ord_range

modified theorem ordinal.eq_enum_ord