list_prod_mem — Mathlib

English

In a submonoid, the Finset product of coerced elements matches the Finset product in the ambient monoid.

Русский

Для подмонома произведение Finset по образам совпадает с произведением в моноиде-окружении.

LaTeX

$$$(f : ι \\to S)\\text{ with Finset } s: \\prod_{i\\in s} (f i) = \\prod_{i\\in s} (f i)$$$

Lean4

/-- Product of a list of elements in a submonoid is in the submonoid. -/
@[to_additive /-- Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`. -/
    ]
theorem list_prod_mem {l : List M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S :=
  by
  lift l to List S using hl
  rw [← coe_list_prod]
  exact l.prod.coe_prop

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