Structures · Algebra

RingHomClass

RingHomClass F α β states that F is a type of (semi)ring homomorphisms. You should extend this class when you extend RingHom. This extends from both MonoidHomClass and MonoidWithZeroHomClass in order to put the fields in a sensible order, even though MonoidWithZeroHomClass already extends MonoidHomClass.

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Shape

3 explicit arguments