Commit 2022-12-15 14:52 ac3910d7

fix(algebra/opposites): fix types in unop_div (#17955) This lemma only typechecked because of defeq abuse, which was presumably not intended. Remark: refactoring mul_opposite to be a structure in Lean 4 was what picked up on this error.