prod_insert_div — Mathlib

English

Let G be a commutative group, ι a type, s a finite subset of ι, and a ∈ ι with a ∉ s. Then (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x. Equivalently, ∏ x ∈ insert a s, f x = f a · ∏ x ∈ s, f x.

Русский

Пусть G — коммутативная группа, ι — множество, s — конечное подмножество ι, a ∈ ι и a ∉ s. Тогда (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x. Эквивалентно, ∏ x ∈ insert a s, f x = f a · ∏ x ∈ s, f x.

LaTeX

$$$$\\left(\\prod_{x \\in s \\cup \\{a\\}} f(x)\\right)/f(a) = \\prod_{x \\in s} f(x)$$$$

Lean4

@[to_additive]
theorem prod_insert_div (ha : a ∉ s) (f : ι → G) : (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x := by simp [ha]

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