Theorems · Definition · ring theory

MulSemiringAction.toRingHom

(M : Type u_1) → [inst : Monoid M] → (R : Type v) → [inst_1 : Semiring R] → [MulSemiringAction M R] → M → R →+* R

Each element of the monoid defines a semiring homomorphism.

Defined in

Mathlib.Algebra.Ring.Action.Basic

Cited by

23 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

MonoidSemiringMulSemiringAction