English
If f is Multipliable, then HasProd f (tprod f L) L.
Русский
Если f мультиплируемое, то HasProd f (tprod f L) L.
LaTeX
$$$ (ha : Multipliable f L) \rightarrow HasProd f (tprod (\lambda b. f b) L) L $$$
Lean4
@[to_additive]
theorem hasProd (ha : Multipliable f L) : HasProd f (∏'[L] b, f b) L := by
-- This is quite delicate because of the fiddly special-casing for finite products.
classical
rw [tprod_def, dif_pos ha]
split_ifs with h h'
· convert hasProd_prod_support_of_ne_finset_one (s := h.2.toFinset) (L := L) _ using 2
· simp only [Set.inter_eq_left.mpr (show ↑h.2.toFinset ⊆ L.support by simp)]
simp only [Set.Finite.coe_toFinset, Finset.toFinset_coe]
rw [finprod_eq_prod_of_mulSupport_subset (s := h.2.toFinset)]
· exact Finset.prod_congr rfl (by aesop)
· simp
· grind [Set.Finite.mem_toFinset, mem_mulSupport]
· exact h.1
· exact h'
· exact ha.choose_spec
