prod_map_erase — Mathlib

English

Let m be a multiset of indices, f a function, and a ∈ m. Then f a · prod((m.erase a).map f) = prod(m.map f).

Русский

Пусть m – мультимножество индексов, f — функция. Тогда f(a) · prod((m.erase a).map f) = prod(m.map f).

LaTeX

$$$ f\ a \cdot \mathrm{prod}(\mathrm{map}\ f\ (m\erase\ a)) = \mathrm{prod}(\mathrm{map}\ f\ m) $$$

Lean4

@[to_additive (attr := simp)]
theorem prod_map_erase [DecidableEq ι] {a : ι} (h : a ∈ m) : f a * ((m.erase a).map f).prod = (m.map f).prod := by
  rw [← m.coe_toList, coe_erase, map_coe, map_coe, prod_coe, prod_coe, List.prod_map_erase f (mem_toList.2 h)]

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