∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} [inst_5 : RingHomInvPair σ₂₃ σ₃₂] [inst_6 : RingHomInvPair σ₃₂ σ₂₃]
  {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_7 : RingHomInvPair σ₁₃ σ₃₁] [inst_8 : RingHomInvPair σ₃₁ σ₁₃]
  [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_10 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4}
  [inst_11 : TopologicalSpace M₁] [inst_12 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_13 : TopologicalSpace M₂]
  [inst_14 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_15 : TopologicalSpace M₃] [inst_16 : AddCommMonoid M₃]
  [inst_17 : Module R₁ M₁] [inst_18 : Module R₂ M₂] [inst_19 : Module R₃ M₃] (e₁ : M₁ ≃SL[σ₁₂] M₂)
  (e₂ : M₂ ≃SL[σ₂₃] M₃), (e₁.trans e₂).toLinearEquiv = e₁.trans e₂.toLinearEquiv