mathlib
66961879 - chore(set_theory/ordinal_arithmetic): Reorder theorems (#12475)

Commit

3 years ago

chore(set_theory/ordinal_arithmetic): Reorder theorems (#12475) It makes more sense for `is_normal.bsup_eq` and `is_normal.blsub_eq` to be together.

Author

vihdzp

Parents