Theorems · Definition · ring theory

MonoidAlgebra.mapRingHom

{R : Type u_3} →
  {S : Type u_4} →
    (M : Type u_6) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] → [inst_2 : Monoid M] → (R →+* S) → MonoidAlgebra R M →+* MonoidAlgebra S M

The ring homomorphism of monoid algebras induced by a homomorphism of the base rings.

Defined in

Mathlib.Algebra.MonoidAlgebra.MapDomain

Cited by

27 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringSemiringMonoid