English
See also smul_finsum' with a more general formulation; essentially the same distributivity for finite support.
Русский
См. также smul_finsum' с более общей формулировкой; по сути та же дистрибутивность для конечной опоры.
LaTeX
$$$\\displaystyle \\text{(same as smul_finsum' with finite support)}$$$
Lean4
/-- A more general version of `MonoidHom.map_finprod_mem` that requires `s ∩ mulSupport f` rather
than `s` to be finite. -/
@[to_additive /-- A more general version of `AddMonoidHom.map_finsum_mem` that requires
`s ∩ support f` rather than `s` to be finite. -/
]
theorem map_finprod_mem' {f : α → M} (g : M →* N) (h₀ : (s ∩ mulSupport f).Finite) :
g (∏ᶠ j ∈ s, f j) = ∏ᶠ i ∈ s, g (f i) := by
rw [g.map_finprod]
· simp only [g.map_finprod_Prop]
· simpa only [finprod_eq_mulIndicator_apply, mulSupport_mulIndicator]
