Theorems · Definition · ring theory

NonUnitalStarRingHom.toNonUnitalRingHom

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

Reinterpret a non-unital star ring homomorphism as a non-unital ring homomorphism by forgetting the interaction with the star operation. Users should not make use of this, but instead utilize the coercion obtained through the NonUnitalRingHomClass instance.

Defined in

Mathlib.Algebra.Star.StarRingHom

Cited by

2 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringStarNonUnitalNonAssocSemiringStar