∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] (σ σ_1 : R →+* S) (e_σ : σ = σ_1)
  {σ' σ'_1 : S →+* R} (e_σ' : σ' = σ'_1) [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] (M : Type u_16)
  (M₂ : Type u_17) [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂],
  (M ≃ₛₗ[σ] M₂) = (M ≃ₛₗ[σ_1] M₂)