Theorems · Definition · ring theory

AlgEquiv.trans

{R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      {A₃ : Type uA₃} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A₁] →
            [inst_2 : Semiring A₂] →
              [inst_3 : Semiring A₃] →
                [inst_4 : Algebra R A₁] →
                  [inst_5 : Algebra R A₂] → [inst_6 : Algebra R A₃] → (A₁ ≃ₐ[R] A₂) → (A₂ ≃ₐ[R] A₃) → A₁ ≃ₐ[R] A₃

Algebra equivalences are transitive.

Defined in

Mathlib.Algebra.Algebra.Equiv

Cited by

108 results in Mathlib

Foundations

Depth 22 from the axioms, rests on 175 definitions · uses Quot.sound

Assumes

CommSemiringSemiringSemiringSemiringAlgebraAlgebraAlgebra