Theorems · Definition · ring theory

RingEquiv.trans

{R : Type u_4} →
  {S : Type u_5} →
    {S' : Type u_6} →
      [inst : Mul R] →
        [inst_1 : Mul S] →
          [inst_2 : Add R] → [inst_3 : Add S] → [inst_4 : Mul S'] → [inst_5 : Add S'] → R ≃+* S → S ≃+* S' → R ≃+* S'

Transitivity of RingEquiv.

Defined in

Mathlib.Algebra.Ring.Equiv

Cited by

54 results in Mathlib

Foundations

Depth 20 from the axioms · uses Quot.sound

Assumes

MulMulAddAddMulAdd