Theorems · Definition · commutative algebra

LinearEquiv.trans

{R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {R₃ : Type u_4} →
      {M₁ : Type u_8} →
        {M₂ : Type u_9} →
          {M₃ : Type u_10} →
            [inst : Semiring R₁] →
              [inst_1 : Semiring R₂] →
                [inst_2 : Semiring R₃] →
                  [inst_3 : AddCommMonoid M₁] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : AddCommMonoid M₃] →
                        {module_M₁ : Module R₁ M₁} →
                          {module_M₂ : Module R₂ M₂} →
                            {module_M₃ : Module R₃ M₃} →
                              {σ₁₂ : R₁ →+* R₂} →
                                {σ₂₁ : R₂ →+* R₁} →
                                  {σ₁₃ : R₁ →+* R₃} →
                                    {σ₃₁ : R₃ →+* R₁} →
                                      {σ₂₃ : R₂ →+* R₃} →
                                        {σ₃₂ : R₃ →+* R₂} →
                                          [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                            [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] →
                                              {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                                                {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} →
                                                  [inst_8 : RingHomInvPair σ₁₃ σ₃₁] →
                                                    {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                                                      {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} →
                                                        [inst_9 : RingHomInvPair σ₃₁ σ₁₃] →
                                                          (M₁ ≃ₛₗ[σ₁₂] M₂) → (M₂ ≃ₛₗ[σ₂₃] M₃) → M₁ ≃ₛₗ[σ₁₃] M₃

Linear equivalences are transitive.

Defined in

Mathlib.Algebra.Module.Equiv.Defs

Cited by

298 results in Mathlib

Foundations

Depth 24 from the axioms, rests on 228 definitions · uses propext, Quot.sound

Assumes

SemiringSemiringSemiringAddCommMonoidAddCommMonoidAddCommMonoidRingHomCompTripleRingHomCompTripleRingHomInvPairRingHomInvPair