toAddConstMapHom — Mathlib

English

There is a monoid hom from AddConstEquiv G G a a to AddConstMap G G a a, given by toAddConstMapHom, i.e., (G ≃+c[a,a] G) →* (G →+c[a,a] G).

Русский

Существует моноидная гомоморфия от AddConstEquiv G G a a к AddConstMap G G a a, заданная toAddConstMapHom.

LaTeX

$$$ \text{toAddConstMapHom} : (G \equiv^+_{a,a} G) \to* (G \to+ c[a,a] G) $$$

Lean4

/-- Projection from `G ≃+c[a, a] G` to `G →+c[a, a] G`, as a monoid homomorphism. -/
@[simps! apply]
def toAddConstMapHom : (G ≃+c[a, a] G) →* (G →+c[a, a] G)
    where
  toFun := toAddConstMap
  map_mul' _ _ := rfl
  map_one' := rfl

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