English
For a magma map f, the domain map commutes with scalar embedding: mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r.
Русский
Для отображения f сохранение домена математики совместимо с вложением скаляра: mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r.
LaTeX
$$$\\operatorname{mapDomain} f\\big(\\mathrm{algebraMap}_k\\big(\\,\\mathrm{MonoidAlgebra} \\; A\\; G\\big)(r)\\big) = \\mathrm{algebraMap}_k\\big(\\mathrm{MonoidAlgebra} \\; A\\; H\\big)(r).$$$
Lean4
@[to_additive]
theorem mapDomain_algebraMap {F : Type*} [FunLike F G H] [MonoidHomClass F G H] (f : F) (r : k) :
mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r := by
simp only [coe_algebraMap, mapDomain_single, map_one, (· ∘ ·)]
