mathlib
159855d1 - feat(set_theory/ordinal_arithmetic): `is_normal.monotone` (#13314)

Commit

3 years ago

feat(set_theory/ordinal_arithmetic): `is_normal.monotone` (#13314) We introduce a convenient abbreviation for `is_normal.strict_mono.monotone`.

Author

vihdzp

Parents