TL;DR: we need an instance from Algebra R A to Module Rᵐᵒᵖ A, and it needs to not create diamonds.

The problem

Mathematically, an $R$-algebra $A$ ([CommSemiring R] [Semiring A] [Algebra R A]) has an obvious action by the commutative $R$. If pushed, we can say that it has obvious left- and right- actions, corresponding to $(r : A)a$ and $a(r : A)$.

However, we can't (and don't) implement things this way in Lean; if we do so, then we end up with instance diamonds, where r • a from some prexisting module structure is not equal to the one defined via the algebra as algebraMap R A r * a.
We've already solved this for left actions; we did this by:

• Making Algebra extend SMul
• Adding Algebra.smul_def to prove that these operations coincide propositionally.
• Adding Algebra.toModule which provides the rest of the algebraic structure, but constructs no new data.

However, mathlib now also has various results about right actions (written Module Rᵐᵒᵖ A), specially left- and right- actions that are compatible in some way. One example is:

instance TrivSqZeroExt.monoid
  {R : Type u} {M : Type v}
  [Monoid R] [AddMonoid M]
  -- M is acted on by `R` on both the left and the right, and the actions associate:
  -- $(r_1 m) r_2 = r_1 (m r_2)$
  [DistribMulAction R M] [DistribMulAction Rᵐᵒᵖ M] [SMulCommClass R Rᵐᵒᵖ M] :
  Monoid (TrivSqZeroExt R M)

This presents a difficulty; this instance can't be applied when M is an Algebra, as there is no instance from Algebra R A to Module Rᵐᵒᵖ A.

Another notable example is Derivation, which if generalized in the same way (as in leanprover-community/mathlib3#18936) would cease to be usable on commutative rings.

The solution

A solution to this in Lean3 is at leanprover-community/mathlib3#10716, which passed CI but was never merged.

The summary is that Algebra needs to gain:

• A SMul Rᵐᵒᵖ A field, to provide the new data needed to make things diamond free
• An Algebra.op_smul_def' x r : op r • x = x * toFun r proof field that shows this is consistent with multiplication
• Adding an instance Algebra.toOppositeModule which provides the rest of the algebraic structure, but constructs no new data.
• Adding an instance Algebra.isCentralScalar : IsCentralScalar R A which follows trivially from Algebra.commutes

This unfortunately creates a new problem: for Algebra ℕ R over some ring, we now need a right-action of ℕ on R, that is defeq to right-multiplication when R = ℕ. Once again, we solved this for left-modules with the AddMonoid.nsmul field; we need to do the same for AddMonoid.op_nsmul. Overall, we will need to add:

• AddMonoid.op_nsmul (and AddMonoid.op_nsmul_eq_nsmul)
• SubtractionMonoid.op_zsmul (and SubtractionMonoid.op_zsmul_eq_zsmul)
• DivisionRing.op_qsmul (and DivisionRing.op_qsmul_eq_qsmul)

Unfortunately, these first two need to match up with the additive versions; so we also need to add op_pow and op_zpow versions too!