mathlib
73513580 - refactor(order/well_founded, set_theory/ordinal_arithmetic): Fix namespace in `self_le_of_strict_mono` (#11871)

Commit
4 years ago
refactor(order/well_founded, set_theory/ordinal_arithmetic): Fix namespace in `self_le_of_strict_mono` (#11871) This places `self_le_of_strict_mono` in the `well_founded` namespace. We also rename `is_normal.le_self` to `is_normal.self_le` .
Author
Parents
Loading