Definition multimodule_ith_mult_0_to_0 {I : UU} {rings : I -> ring} {MM : multimodule rings} (i : I) (x : MM) : multimodule_ith_mult MM i (@ringunel1 (rings i)) x = @unel MM := @module_mult_0_to_0 (rings i) (ith_module MM i) x.
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.