prod_subset_one_on_sdiff — Mathlib

English

If s1 ⊆ s2 and the elements in s2\\s1 map to 1 under g, and f agrees with g on s1, then the products over s1 and s2 under f and g are equal.

Русский

Если s1 ⊆ s2 и элементы в s2\\s1 отправляются в 1 под g, а на s1 f и g совпадают, тогда произведения совпадают.

LaTeX

$$$\\prod_{i \\in s_1} f(i) = \\prod_{i \\in s_2} g(i)$ under given conditions$$

Lean4

@[to_additive]
theorem prod_subset_one_on_sdiff [DecidableEq ι] (h : s₁ ⊆ s₂) (hg : ∀ x ∈ s₂ \ s₁, g x = 1)
    (hfg : ∀ x ∈ s₁, f x = g x) : ∏ i ∈ s₁, f i = ∏ i ∈ s₂, g i :=
  by
  rw [← prod_sdiff h, prod_eq_one hg, one_mul]
  exact prod_congr rfl hfg

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