∀ {R M : Type u_1} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ)
  (x y : (AlgebraicGeometry.structureSheafInType R R).obj.obj U)
  (b : (AlgebraicGeometry.structureSheafInType R M).obj.obj U), (x * y) • b = x • y • b