list_prod_apply — Mathlib

English

If x and y are equal in the π-space, then the product over x equals the product over y equals 1.

Русский

Если x и y равны в пространстве π, то произведение по x равно произведению по y и равно единице.

LaTeX

$$$\\forall {x y : (π C (· ∈ s)) .Elem}, (h : y = x) \\Rightarrow (factors C s x).prod y = 1$$$

Lean4

theorem list_prod_apply {I} (C : Set (I → Bool)) (x : C) (l : List (LocallyConstant C ℤ)) :
    l.prod x = (l.map (LocallyConstant.evalMonoidHom x)).prod := by
  rw [← map_list_prod (LocallyConstant.evalMonoidHom x) l, LocallyConstant.evalMonoidHom_apply]

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