∀ (S : Type u_2) (R : Type u_3) (M : Type u_1) [inst : CommSemiring S] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Algebra S R] [inst_4 : Module S M] [inst_5 : Module R M] [inst_6 : Module Rᵐᵒᵖ M] [IsScalarTower S R M]
  (s : S) (x : TrivSqZeroExt R M), s • x.snd = (algebraMap S R) s • x.snd + MulOpposite.op x.fst • 0