Theorems · Definition · ring theory

NonUnitalRingHom.toMulHom

{α : Type u_5} →
  {β : Type u_6} → [inst : NonUnitalNonAssocSemiring α] → [inst_1 : NonUnitalNonAssocSemiring β] → (α →ₙ+* β) → α →ₙ* β

Reinterpret a non-unital ring homomorphism f : α →ₙ+* β as a semigroup homomorphism α →ₙ* β. The simp-normal form is (f : α →ₙ* β).

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

15 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring