finprod_eq_single — Mathlib

English

If f x = 1 for all x ≠ a, then the finprod equals f a.

Русский

Если для всех x ≠ a выполняется f x = 1, то финпроизведение равно f a.

LaTeX

$$$\\big(\\forall x\\ne a, f x = 1\\big) \\Rightarrow \\mathrm{finprod}(f) = f(a)$$$

Lean4

@[to_additive]
theorem finprod_eq_single (f : α → M) (a : α) (ha : ∀ x, x ≠ a → f x = 1) : ∏ᶠ x, f x = f a :=
  by
  have : mulSupport (f ∘ PLift.down) ⊆ ({PLift.up a} : Finset (PLift α)) :=
    by
    intro x
    contrapose
    simpa [PLift.eq_up_iff_down_eq] using ha x.down
  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_singleton]

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