mulAction — Mathlib

English

If each αi carries a MulAction M on αi, then the Pi-type ∀i αi carries a MulAction M defined pointwise by (m • f)(i) = m • f(i).

Русский

Пусть на каждом αi задано действие MulAction M. Тогда на ∀i αi будет естественно задано действие M по координатам: (m • f)(i) = m • f(i).

LaTeX

$$$\text{MulAction } M\big(\forall i\, \alpha_i\big)\text{ with } (m\cdot f)(i) = m\cdot f(i).$$$

Lean4

@[to_additive]
instance mulAction (M) {m : Monoid M} [∀ i, MulAction M (α i)] : @MulAction M (∀ i, α i) m
    where
  smul := (· • ·)
  mul_smul _ _ _ := funext fun _ ↦ mul_smul _ _ _
  one_smul _ := funext fun _ ↦ one_smul _ _

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