Theorems · Definition · ring theory

MulSemiringAction.toAlgHom

{M : Type u_1} →
  (R : Type u_3) →
    (A : Type u_4) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Monoid M] → [inst_4 : MulSemiringAction M A] → [SMulCommClass M R A] → M → A →ₐ[R] A

Each element of the monoid defines an algebra homomorphism. This is a stronger version of MulSemiringAction.toRingHom and DistribSMul.toLinearMap.

Defined in

Mathlib.Algebra.Algebra.Hom

Cited by

10 results in Mathlib

Foundations

Depth 21 from the axioms · uses no axioms

Assumes

CommSemiringSemiringAlgebraMonoidMulSemiringActionSMulCommClass