mathlib3

ac3910d7 - fix(algebra/opposites): fix types in unop_div (#17955)

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.