Commit 2022-02-02 14:51 307a456f
View on Github →refactor(set_theory/ordinal): Add covariant_class instances for ordinal addition and multiplication (#11678)
This replaces the old add_le_add_left, add_le_add_right, mul_le_mul_left, mul_le_mul_right theorems.