Commit 2022-09-29 01:02 0ec98ed0
View on Github →refactor(data/real/ereal): sub_neg_zero_monoid
instance (#16688)
Add a sub_neg_zero_monoid
instance for ereal
, so eliminating its neg_zero
, sub_zero
and sub_eq_add_neg
lemmas and allowing results for neg_zero_class
to be applied to ereal
.