Commit 2022-09-29 16:43 c8760bde
View on Github →refactor(algebra/ring/basic): replace neg_zero' by neg_zero_class instance (#16686)
Eliminate the separate neg_zero' lemma for the combination of mul_zero_class with has_distrib_neg by adding a neg_zero_class instance for that case.