fact: Definition bimodule_struct' (R S : ring) (G : abgr) : UU := ∑ (mr : module_struct R G) (ms : module_struct (S⁰) G), let mulr := module_mult (G,, mr) in let muls := module_mult (G,, ms) in ∏ (r : R) (s : S), mulr r ∘ muls s = muls s ∘ mulr r.
imports: UniMath.Algebra.Modules.Core UniMath.Algebra.Modules.Multimodules UniMath.Algebra.Monoids UniMath.Algebra.Groups UniMath.Algebra.RigsAndRings UniMath.Foundations.Preamble UniMath.MoreFoundations.Tactics