comapDistribMulAction — Mathlib

English

If G is a monoid acting on α and α →₀ M is given an action by comapSMul, then this induces a distributive action of G on α →₀ M; in particular smul_zero and smul_add hold.

Русский

Если G — моноид, действующий на α, и на α →₀ M задано действие через comapSMul, то это порождает распределённое действие G на α →₀ M; в частности выполняются свойства smul_zero и smul_add.

LaTeX

$$$\text{DistribMulAction } G\, (\alpha \\to_0 M)$$$

Lean4

/-- `Finsupp.comapSMul` is distributive -/
def comapDistribMulAction : DistribMulAction G (α →₀ M)
    where
  smul_zero
    g := by
    ext a
    simp only [comapSMul_def]
    simp
  smul_add g f
    f' := by
    ext
    simp only [comapSMul_def]
    simp [mapDomain_add]

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