Theorems · Definition · ring theory

MonoidAlgebra.mapDomain

{R : Type u_3} → {M : Type u_6} → {N : Type u_7} → [inst : Semiring R] → (M → N) → MonoidAlgebra R M → MonoidAlgebra 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

15 results in Mathlib

Foundations

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

Assumes

Semiring