English
As above, but using finsum instead of finite summation; (f*g).coeff x equals the finsum over p in {p : G×G | p.1·p.2 = x} of f.coeff p.1 · p.1 • g.coeff p.2.
Русский
Как выше, но через finsum; (f*g).coeff x равен finsum по p ∈ {p : G×G | p.1·p.2 = x} от f.coeff p.1 · p.1 • g.coeff p.2.
LaTeX
$$$ (f * g).\mathrm{coeff}(x) = \sum^\!\!_p f_{p.1} \; p.1 \cdot g_{p.2} \quad (p.1 \cdot p.2 = x)$$$
Lean4
/-- If f : G → H is a multiplicative homomorphism between two monoids and
`∀ (a : G) (x : k), a • x = (f a) • x`, then `mapDomain f` is a ring homomorphism
between their skew monoid algebras. -/
def mapDomainRingHom [MulSemiringAction α β] [MulSemiringAction α₂ β] [MonoidHomClass F α α₂] {f : F}
(hf : ∀ (a : α) (x : β), a • x = (f a) • x) : SkewMonoidAlgebra β α →+* SkewMonoidAlgebra β α₂
where
__ := (mapDomain f : SkewMonoidAlgebra β α →+ SkewMonoidAlgebra β α₂)
map_one' := mapDomain_one f
map_mul' x y := mapDomain_mul x y hf
