English
If HasProd f a L and HasProd (ite (n=b) 1 (f n)) a' L, then a = a' · f(b).
Русский
Если HasProd f на a и HasProd ite выражение даёт a', то a = a' · f(b).
LaTeX
$$a = a' * f(b)$$
Lean4
/-- Version of `hasProd_ite_div_hasProd` for `CommMonoid` rather than `CommGroup`.
Rather than showing that the `ite` expression has a specific product in terms of `HasProd`, it gives
a relationship between the products of `f` and `ite (n = b) 0 (f n)` given that both exist. -/
@[to_additive /-- Version of `hasSum_ite_sub_hasSum` for `AddCommMonoid` rather than `AddCommGroup`.
Rather than showing that the `ite` expression has a specific sum in terms of `HasSum`,
it gives a relationship between the sums of `f` and `ite (n = b) 0 (f n)` given that both exist. -/
]
theorem eq_mul_of_hasProd_ite [L.LeAtTop] [L.NeBot] {α : Type*} [TopologicalSpace α] [CommMonoid α] [T2Space α]
[ContinuousMul α] [DecidableEq β] {f : β → α} {a : α} (hf : HasProd f a L) (b : β) (a' : α)
(hf' : HasProd (fun n ↦ ite (n = b) 1 (f n)) a' L) : a = a' * f b :=
by
refine (mul_one a).symm.trans (hf.update' b 1 ?_)
convert hf'
apply update_apply
