∀ (G : Type u_2) (R : Type u_1) [inst : Group G] [inst_1 : Semiring R] [inst_2 : MulSemiringAction G R] (g h : G),
  MulSemiringAction.toRingEquiv G R (g * h) = MulSemiringAction.toRingEquiv G R g * MulSemiringAction.toRingEquiv G R h