Theorems · Definition · ring theory

RingHom.toMonoidWithZeroHom

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

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

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

24 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

NonAssocSemiringNonAssocSemiring