English
Let α be an additive commutative monoid and f a map from α to some monoid M. Translating the index of a finite product over the interval Ico(a,b) by c yields the same product over Ico(a+c, b+c): ∏_{x∈Ico(a,b)} f(x+c) = ∏_{x∈Ico(a+c,b+c)} f(x).
Русский
Пусть α—коммутативное аддитивное моноид, f: α → M. При сдвиге индекса на c произведение по интервалу Ico(a,b) сохраняется: ∏_{x∈Ico(a,b)} f(x+c) = ∏_{x∈Ico(a+c,b+c)} f(x).
LaTeX
$$$$ \\displaystyle \\prod_{x \\in \\mathrm{Ico}(a,b)} f(x+c) = \\prod_{x \\in \\mathrm{Ico}(a+c,b+c)} f(x). $$$$
Lean4
@[to_additive]
theorem prod_Ico_add' [AddCommMonoid α] [PartialOrder α] [IsOrderedCancelAddMonoid α] [ExistsAddOfLE α]
[LocallyFiniteOrder α] (f : α → M) (a b c : α) : (∏ x ∈ Ico a b, f (x + c)) = ∏ x ∈ Ico (a + c) (b + c), f x :=
by
rw [← map_add_right_Ico, prod_map]
rfl
