Definition arecompatibleactions {R S G} (mr : module_struct R G) (ms : module_struct S G) := let m1 := module_mult (G,, mr) in let m2 := module_mult (G,, ms) in ∏ (r1 : R) (r2 : S), (m1 r1 ∘ m2 r2 = m2 r2 ∘ m1 r1)%functions.
Require Import UniMath.Algebra.Modules.Core. Require Import UniMath.Algebra.Groups. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Sets.