Theorems · Inductive type · ring theory

NonUnitalRingHomClass

(F : Type u_5) →
  (α : outParam (Type u_6)) →
    (β : outParam (Type u_7)) → [NonUnitalNonAssocSemiring α] → [NonUnitalNonAssocSemiring β] → [FunLike F α β] → Prop

NonUnitalRingHomClass F α β states that F is a type of non-unital (semi)ring homomorphisms. You should extend this class when you extend NonUnitalRingHom.

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

82 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiringFunLike