mulActionFinset — Mathlib

English

There is a canonical MulAction α on Finset β given by the pointwise action, compatible with Finset’s structure.

Русский

Существует каноническое действие Finset β моноида α, согласованное с конструкцией Finset.

LaTeX

$$$MulAction\ α\ (Finset\ β).$$$

Lean4

/-- A multiplicative action of a monoid on a type `β` gives a multiplicative action on `Finset β`.
-/
@[to_additive /-- An additive action of an additive monoid on a type `β` gives an additive action
          on `Finset β`. -/
    ]
protected def mulActionFinset [Monoid α] [MulAction α β] : MulAction α (Finset β) :=
  coe_injective.mulAction _ coe_smul_finset

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