Theorems · Definition · ring theory

SkewMonoidAlgebra.mapDomain

{k : Type u_1} →
  {G : Type u_2} →
    [inst : AddCommMonoid k] → {G' : Type u_3} → (G → G') → SkewMonoidAlgebra k G →+ SkewMonoidAlgebra k G'

Given f : G → G' and v : SkewMonoidAlgebra k G, mapDomain f v : SkewMonoidAlgebra k G' is the finitely supported additive homomorphism whose value at a : G' is the sum of v x over all x such that f x = a. Note that SkewMonoidAlgebra.mapDomain is defined as an AddHom, while MonoidAlgebra.mapDomain is defined as a function.

Defined in

Mathlib.Algebra.SkewMonoidAlgebra.Basic

Cited by

12 results in Mathlib

Foundations

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

Assumes

AddCommMonoid