Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 05:19 174f1da1

View on Github →

refactor(set_theory/ordinal_arithmetic): Turn various results into simp lemmas (#12661) In order to do this, we had to change the direction of various equalities.

Estimated changes

modified theorem ordinal.blsub_eq_lsub'
modified theorem ordinal.blsub_eq_lsub
added theorem ordinal.bsup_eq_blsub
modified theorem ordinal.bsup_eq_sup'
modified theorem ordinal.bsup_eq_sup
modified theorem ordinal.lsub_eq_blsub'
modified theorem ordinal.lsub_eq_blsub
modified theorem ordinal.sup_eq_bsup'
modified theorem ordinal.sup_eq_bsup
added theorem ordinal.sup_eq_lsub