distribSMul — Mathlib

English

If the scalar action is distributive on β, then it is distributive on Finset β by transporting the operation through the set-powerset representation.

Русский

Если скалярное умножение распределимо действует на β, то оно распределимо действует и на Finset β образуя соответствующую структуру.

LaTeX

$$$\text{Finset.distribSMul}:\; DistribSMul α (Finset β)$ given distributive action on β.$$

Lean4

/-- If the scalar multiplication `(· • ·) : α → β → β` is distributive,
then so is `(· • ·) : α → Finset β → Finset β`. -/
protected noncomputable def distribSMul [AddZeroClass β] [DistribSMul α β] : DistribSMul α (Finset β) :=
  coe_injective.distribSMul coeAddMonoidHom coe_smul_finset

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