Theorems · Definition · ring theory

RingHom.toAddMonoidHom

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

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

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

17 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

NonAssocSemiringNonAssocSemiring