MulOpposites and [instances]

Stream: Is there code for X?

[Damiano Testa]

Dear All,

in mathlib4, the implementation of Mul/AddOpposites changed wrt mathlib3 and I am not yet famliar with the setup.

Is the instance below available? Usable? Desirable? Of course, there are plenty more, in case this one is missing!

import Mathlib.Algebra.Opposites
import Mathlib.Algebra.Group.Defs
import Mathlib.Tactic.ApplyFun

open MulOpposite
instance {A : Type*} [inst : Mul A] [inst_1 : IsLeftCancelMul A] : IsRightCancelMul Aᵐᵒᵖ :=
⟨fun a b c bc => by
  apply_fun unop at bc ⊢ using unop_injective (α := A)
  exact mul_left_cancel bc⟩

[Eric Wieser]

I think it's just missing

[Eric Wieser]

I think the stronger CancelMonoid-like classes are there

[Damiano Testa]

I'll PR it soon, then!

Unless @Junyan Xu wants to beat me to it! (This is for the PR on NoZeroDivisors.)

[Damiano Testa]

For reference, docs#MulOpposite.addSemigroup and around there is what Eric was saying, I believe.

[Damiano Testa]

Even though, Mul...add is a little strange. Seems like to_additive is missing a trick!

[Damiano Testa]

#6752