Theorems · Definition · ring theory

AddMonoidAlgebra.mapDomain

{R : Type u_3} →
  {M : Type u_6} → {N : Type u_7} → [inst : Semiring R] → (M → N) → AddMonoidAlgebra R M → AddMonoidAlgebra R N

Given a function f : M → N between magmas, return the corresponding map R[M] → R[N] obtained by summing the coefficients along each fiber of f.

Defined in

Mathlib.Algebra.MonoidAlgebra.MapDomain

Cited by

17 results in Mathlib

Foundations

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

Assumes

Semiring