English
A multiplicative action of a monoid α on a type β induces a multiplicative action of Finset α on Finset β, defined by image₂ (coordinatewise).
Русский
Действие по умножению моноида α на β порождает соответствующее действие на Finset α на Finset β, задаваемое образованием по координатам.
LaTeX
$$$MulAction\ α\ (Finset\ β).$$$
Lean4
/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of
`Finset α` on `Finset β`. -/
@[to_additive /-- An additive action of an additive monoid `α` on a type `β` gives an additive action
of `Finset α` on `Finset β` -/
]
protected def mulAction [DecidableEq α] [Monoid α] [MulAction α β] : MulAction (Finset α) (Finset β)
where
mul_smul _ _ _ := image₂_assoc mul_smul
one_smul s := image₂_singleton_left.trans <| by simp_rw [one_smul, image_id']
