Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-06 07:44 b7808a99

View on Github →

chore(set_theory/ordinal_arithmetic): Golf lsub_typein and blsub_id (#12203)

Estimated changes

modified theorem ordinal.blsub_id
modified theorem ordinal.bsup_id_limit
modified theorem ordinal.bsup_id_succ
modified theorem ordinal.lsub_typein
modified theorem ordinal.sup_typein_succ