English
Equality of central-scalar properties lifts to Set β: Set β is a central scalar object.
Русский
Свойство центрального скаляра поднимается на множество β: множество β является центральным скаляром.
LaTeX
$$$ IsCentralScalar α (Set β) $$$
Lean4
/-- A multiplicative action of a monoid `α` on a type `β` gives a multiplicative action of `Set α`
on `Set β`. -/
@[to_additive /-- An additive action of an additive monoid `α` on a type `β` gives an additive action of `Set α`
on `Set β` -/
]
protected noncomputable def mulAction [Monoid α] [MulAction α β] : MulAction (Set α) (Set β)
where
mul_smul _ _ _ := image2_assoc mul_smul
one_smul s := image2_singleton_left.trans <| by simp_rw [one_smul, image_id']
