mathlib

e8858fdd - refactor(algebra/opposites): use mul_opposite for multiplicative opposite (#10302)

refactor(algebra/opposites): use mul_opposite for multiplicative opposite (#10302) Split out `mul_opposite` from `opposite`, to leave room for an `add_opposite` in future. Multiplicative opposites are now spelt `Aᵐᵒᵖ` instead of `Aᵒᵖ`. `Aᵒᵖ` now refers to the categorical opposite. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>