piFinset_smul — Mathlib

English

Discrete product smul distributes for Finset indexed by a finite type: piFinset (i ↦ s i • t i) = s • piFinset t.

Русский

Дискретное произведение через smul распределяется для Finset, индексируемого конечным типом: piFinset (i ↦ s i • t i) = s • piFinset t.

LaTeX

$$$\\pi\\mathrm{Finset} (i \\mapsto s_i \\cdot t_i) = s \\cdot \\pi\\mathrm{Finset} t$$$

Lean4

@[to_additive]
theorem piFinset_smul [∀ i, SMul (α i) (β i)] (s : ∀ i, Finset (α i)) (t : ∀ i, Finset (β i)) :
    piFinset (fun i ↦ s i • t i) = piFinset s • piFinset t :=
  piFinset_image₂ _ _ _

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