Theorems · Definition · ring theory

NonUnitalRingHom.toAddMonoidHom

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

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

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

3 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring