{M : Type u_9} →
  {N : Type u_10} →
    [inst : Monoid M] →
      [inst_1 : Monoid N] →
        (smul : M → N → N) →
          (∀ (x y : M) (b : N), (x * y) • b = x • y • b) →
            (∀ (b : N), 1 • b = b) →
              (∀ (r : M) (x y : N), r • (x * y) = r • x * r • y) → (∀ (r : M), r • 1 = 1) → MulDistribMulAction M N