piFinset_smul_finset — Mathlib

English

In a finite index family of types, the piFinset of smuls equals smul of piFinset.

Русский

В крайней мере для конечной размерности пи-финсет: пи-финсет умножает через smul на финсет.

LaTeX

$$$\\pi\\mathrm{Finset} (i \\mapsto a_i \\cdot s_i) = a \\cdot \\pi\\mathrm{Finset} s$$$

Lean4

@[to_additive]
theorem piFinset_smul_finset [∀ i, SMul (α i) (β i)] (a : ∀ i, α i) (s : ∀ i, Finset (β i)) :
    piFinset (fun i ↦ a i • s i) = a • piFinset s :=
  piFinset_image _
    _
      -- Note: We don't currently state `piFinset_vsub` because there's no
      -- `[∀ i, VSub (β i) (α i)] → VSub (∀ i, β i) (∀ i, α i)` instance

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