Theorems · Definition · ring theory

RingHom.comp

{α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      {x : NonAssocSemiring α} →
        {x_1 : NonAssocSemiring β} → {x_2 : NonAssocSemiring γ} → (β →+* γ) → (α →+* β) → α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

899 results in Mathlib

Foundations

Depth 18 from the axioms, rests on 149 definitions · uses propext, Quot.sound