English
The mapDomain abbreviation defines the monoid-algebra map by applying f to coefficients along fibers of a function f: M → N.
Русский
Аббревюра mapDomain задаёт отображение моноидной алгебры путём применения f к коэффициентам по фибрам функции f: M → N.
LaTeX
$$$ \text{mapDomain} (f) (v) := Finsupp.mapDomain f v $$$
Lean4
/-- 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`. -/
@[to_additive /-- 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`. -/
]
abbrev mapDomain (f : M → N) (v : MonoidAlgebra R M) : MonoidAlgebra R N :=
Finsupp.mapDomain f v
