Theorems · Definition · ring theory

AddMonoidAlgebra.mapRingHom

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

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

Defined in

Mathlib.Algebra.MonoidAlgebra.MapDomain

Cited by

17 results in Mathlib

Foundations

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

Assumes

SemiringSemiringAddMonoid