toAddMonoidEnd — Mathlib

English

The integers act on A in a way that commutes with the M-action: for all n ∈ Z, m ∈ M, a ∈ A, we have n • (m • a) = m • (n • a).

Русский

Целые числа действуют на A так, что действие целых чисел коммутабельно с действием M: для всех n∈Z, m∈M, a∈A имеет место n • (m • a) = m • (n • a).

LaTeX

$$$\forall n \in \mathbb{Z}, \forall m \in M, \forall a \in A,\; n \cdot (m \cdot a) = m \cdot (n \cdot a)$$$

Lean4

/-- Each element of the monoid defines an additive monoid homomorphism. -/
@[simps]
def toAddMonoidEnd : M →* AddMonoid.End A
    where
  toFun := DistribMulAction.toAddMonoidHom A
  map_one' := AddMonoidHom.ext <| one_smul M
  map_mul' x y := AddMonoidHom.ext <| mul_smul x y

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