Theorems · Definition · ring theory

NonUnitalRingHom.comp

{α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : NonUnitalNonAssocSemiring α] →
        [inst_1 : NonUnitalNonAssocSemiring β] →
          [inst_2 : NonUnitalNonAssocSemiring γ] → (β →ₙ+* γ) → (α →ₙ+* β) → α →ₙ+* γ

Composition of non-unital ring homomorphisms is a non-unital ring homomorphism.

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

38 results in Mathlib

Foundations

Depth 15 from the axioms · uses propext, Quot.sound

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiringNonUnitalNonAssocSemiring