toMonoidHom — Mathlib

English

For a monoid M acting on a, the map r ↦ (a ↦ r • a) defines a monoid homomorphism from M to End(A).

Русский

Для моноида M, действующего на A, отображение r ↦ (a ↦ r • a) задаёт моноидный гомоморфизм M → End(A).

LaTeX

$$$ \text{toMonoidEnd } : M \to^* \text{MonoidEnd } A, \quad (r \mapsto (a \mapsto r \cdot a)). $$$

Lean4

/-- Scalar multiplication by `r` as a `MonoidHom`. -/
@[simps]
def toMonoidHom (r : M) : A →* A where
  toFun := (r • ·)
  map_one' := smul_one r
  map_mul' := smul_mul' r

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