Theorems · Definition · ring theory

NonUnitalStarRingHom.comp

{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : NonUnitalNonAssocSemiring A] →
        [inst_1 : Star A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [inst_3 : Star B] →
              [inst_4 : NonUnitalNonAssocSemiring C] → [inst_5 : Star C] → (B →⋆ₙ+* C) → (A →⋆ₙ+* B) → A →⋆ₙ+* C

The composition of non-unital ⋆-ring homomorphisms, as a non-unital ⋆-ring homomorphism.

Defined in

Mathlib.Algebra.Star.StarRingHom

Cited by

8 results in Mathlib

Foundations

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

Assumes

NonUnitalNonAssocSemiringStarNonUnitalNonAssocSemiringStarNonUnitalNonAssocSemiringStar