finprod_one — Mathlib

English

Same as List.prod_ofFn: the product of List.ofFn f equals the product over all i of f i.

Русский

Тоже, что List.ofFn: произведение List.ofFn f равно произведению по всем i от f i.

LaTeX

$$$\\mathrm{List.ofFn}\\ f\\.prod = \\prod_{i} f(i)$$$

Lean4

@[to_additive (attr := simp)]
theorem finprod_one : (∏ᶠ _ : α, (1 : M)) = 1 :=
  by
  have : (mulSupport fun x : PLift α => (fun _ => 1 : α → M) x.down) ⊆ (∅ : Finset (PLift α)) := fun x h => by simp at h
  rw [finprod_eq_prod_plift_of_mulSupport_subset this, Finset.prod_empty]

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