English
If two finite sets s1 and s2 share the same elements on the intersection and outside the intersection they are matched by equal values (with 1 on the excluded parts), then the products are equal.
Русский
Если две конечные множества имеют одинаковые значения на пересечении и совпадают вне пересечения (с равенством 1 на исключённых частях), то их произведения равны.
LaTeX
$$$\forall a, a\in s1, a\in s2 \to f a = g a \,\Rightarrow\, \prod_{a\in s1} f a = \prod_{a\in s2} g a$$$
Lean4
/-- The products of two functions `f g : ι → M` over finite sets `s₁ s₂ : Finset ι`
are equal if the functions agree on `s₁ ∩ s₂`, `f = 1` and `g = 1` on the respective
set differences. -/
@[to_additive /-- The sum of two functions `f g : ι → M` over finite sets `s₁ s₂ : Finset ι`
are equal if the functions agree on `s₁ ∩ s₂`, `f = 0` and `g = 0` on the respective
set differences. -/
]
theorem prod_congr_of_eq_on_inter {ι M : Type*} {s₁ s₂ : Finset ι} {f g : ι → M} [CommMonoid M]
(h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) (h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1) (h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a) :
∏ a ∈ s₁, f a = ∏ a ∈ s₂, g a := by
classical
conv_lhs => rw [← sdiff_union_inter s₁ s₂, prod_union_eq_right (by simp_all)]
conv_rhs => rw [← sdiff_union_inter s₂ s₁, prod_union_eq_right (by simp_all), inter_comm]
exact prod_congr rfl (by simpa)
