addLeftHom — Mathlib

English

The map c ↦ (translation by c) defines a monoid homomorphism from Multiplicative G to AddConstMap G G a a.

Русский

Отображение, отправляющее элемент c на переход на c (постоянная карта), образует моноидовый гомоморфизм из Multiplicative G в AddConstMap G G a a.

LaTeX

$$$\text{addLeftHom}: Multiplicative G \to* (G \to+c[a,a] G),\; c \mapsto (x \mapsto x + c).$$$

Lean4

/-- The map that sends `c` to a translation by `c`
as a monoid homomorphism from `Multiplicative G` to `G →+c[a, a] G`. -/
@[simps! -fullyApplied]
def addLeftHom : Multiplicative G →* (G →+c[a, a] G)
    where
  toFun c := c.toAdd +ᵥ .id
  map_one' := by ext; apply zero_add
  map_mul' _ _ := by ext; apply add_assoc

Похожие утверждения