Commit 2022-02-14 10:22 dce5dd4c
View on Github →feat(order/well_founded, set_theory/ordinal_arithmetic): eq_strict_mono_iff_eq_range (#11882)
Two strict monotonic functions with well-founded domains are equal iff their ranges are. We use this to golf eq_enum_ord.