Commit 2023-05-23 20:29 598588db

refactor: make MulOpposite = AddOpposite (#4050) It turns out to be convenient to have MulOpposite α = AddOpposite α true by definition, in the same way that it is convenient to have Additive α = α; this means that we also get the defeq AddOpposite (Additive α) = MulOpposite α, which is convenient when working with quotients. This is a compromise between making MulOpposite α = AddOpposite α = α (what we had in Lean 3) and having no defeqs within those three types (which we had as of #1036). This is motivated by #3333