English
A variant showing that the Pi-type of function spaces inherits a MulDistribMulAction structure componentwise for families of monoids with distributive action.
Русский
Вариант, демонстрирующий, что Π-тип функций наследует структуру MulDistribMulAction покомпонентно для семейств моноидов с распределённым действием.
LaTeX
$$$\text{If } \forall i, f(i) \text{ and } g(i) \text{ are Monoid and } DistribMulAction, \; \forall i, MulDistribMulAction (f(i)) (g(i)) \Rightarrow MulDistribMulAction ((i) \mapsto f(i)) ((i) \mapsto g(i)).$$$
Lean4
instance mulDistribMulAction' {g : I → Type*} {m : ∀ i, Monoid (f i)} {n : ∀ i, Monoid <| g i}
[∀ i, MulDistribMulAction (f i) (g i)] :
@MulDistribMulAction (∀ i, f i) (∀ i : I, g i) (@Pi.monoid I f m) (@Pi.monoid I g n)
where
smul_mul := by
intros
ext x
apply smul_mul'
smul_one := by
intros
ext x
apply smul_one
