prod_eq_mul_of_mem — Mathlib

English

If a,b ∈ s, a ≠ b and all other c ∈ s satisfy f c = 1, then the product equals f a · f b.

Русский

Если a,b ∈ s, a ≠ b и все прочие c ∈ s дают f c = 1, тогда произведение равно f a · f b.

LaTeX

$$$\prod x\in s, f x = f a \cdot f b$$$

Lean4

@[to_additive]
theorem prod_eq_mul_of_mem {s : Finset ι} {f : ι → M} (a b : ι) (ha : a ∈ s) (hb : b ∈ s) (hn : a ≠ b)
    (h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) : ∏ x ∈ s, f x = f a * f b :=
  by
  haveI := Classical.decEq ι; let s' := ({ a, b } : Finset ι)
  have hu : s' ⊆ s := by grind
  have hf : ∀ c ∈ s, c ∉ s' → f c = 1 := by grind
  rw [← Finset.prod_subset hu hf]
  exact Finset.prod_pair hn

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