mulDistribMulActionSet — Mathlib

English

A distributive action of a monoid α on a monoid β yields a distributive action on Set β; i.e., a • (X · Y) = (a • X) · (a • Y) and a • {1} = {1}.

Русский

Распространённое действие моноида α на моноид β порождает распределённое действие на Set β; т.е. a • (X · Y) = (a • X) · (a • Y) и a • {1} = {1}.

LaTeX

$$$ a \cdot (X Y) = (a \cdot X) (a \cdot Y), \quad a \cdot \{1\} = \{1\} $$$

Lean4

/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`. -/
protected noncomputable def mulDistribMulActionSet [Monoid α] [Monoid β] [MulDistribMulAction α β] :
    MulDistribMulAction α (Set β)
    where
  smul_mul _ _ _ := image_image2_distrib <| smul_mul' _
  smul_one _ := image_singleton.trans <| by rw [smul_one, singleton_one]

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