Theorems · Inductive type · ring theory

NonUnitalRingHom

(α : Type u_5) → (β : Type u_6) → [NonUnitalNonAssocSemiring α] → [NonUnitalNonAssocSemiring β] → Type (max u_5 u_6)

Bundled non-unital semiring homomorphisms α →ₙ+* β; use this for bundled non-unital ring homomorphisms too. When possible, instead of parametrizing results over (f : α →ₙ+* β), you should parametrize over (F : Type*) [NonUnitalRingHomClass F α β] (f : F). When you extend this structure, make sure to extend NonUnitalRingHomClass.

Defined in

Mathlib.Algebra.Ring.Hom.Defs

Cited by

157 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 2 definitions · uses no axioms

Assumes

NonUnitalNonAssocSemiringNonUnitalNonAssocSemiring