distribMulAction — Mathlib

English

Dependent functions with finite support inherit a distributive multiplicative action from each coordinate.

Русский

Функции с конечной опорой унаследуют распределимое действие умножения от каждой координаты.

LaTeX

$$$$ \\text{DistribMulAction}(\\gamma, (β_i)) $$$$

Lean4

/-- Dependent functions with finite support inherit a `DistribMulAction` structure from such a
structure on each coordinate. -/
instance distribMulAction [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] :
    DistribMulAction γ (Π₀ i, β i) :=
  Function.Injective.distribMulAction coeFnAddMonoidHom DFunLike.coe_injective coe_smul

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