English
If M is a monoid and α is a type with an M-action, then M acts on the type Option α by applying the action to the contained value; 1 acts as identity and multiplication distributes over nested Options.
Русский
Если M — моноид и α имеет действие M, тогда M действует на тип Option α: действие применяется к содержимому; единица действует как тождественный оператор, а умножение распределяется над вложенными значениями.
LaTeX
$$$$\text{instMulAction: } M \times (Option\;\alpha) \to Option\;\alpha,\; 1 \cdot b = b,\; (a_1 a_2) \cdot b = a_1 \cdot (a_2 \cdot b). $$$$
Lean4
instance [Monoid M] [MulAction M α] : MulAction M (Option α)
where
smul := (· • ·)
one_smul
b := by
cases b
exacts [rfl, congr_arg some (one_smul _ _)]
mul_smul a₁ a₂
b := by
cases b
exacts [rfl, congr_arg some (mul_smul _ _ _)]
