prod_map_eq_pow_single — Mathlib

English

Let i be an index and f a function with DecidableEq; then (m.map (λ i, f i)^n).prod = (m.map f).prod^n.

Русский

Пусть i — индекс, f — функция, степень n; тогда произведение по компонентам после возведения в степень n равно степени произведения по компонентам: prod((map f i)^n) = (prod(map f))^n.

LaTeX

$$$ \mathrm{prod}(\mathrm{map}(\lambda i. f i)\, m)^{n} = \mathrm{prod}(\mathrm{map}(\lambda i. f i)\, m)^n $$$

Lean4

@[to_additive]
theorem prod_map_eq_pow_single [DecidableEq ι] (i : ι) (hf : ∀ i' ≠ i, i' ∈ m → f i' = 1) :
    (m.map f).prod = f i ^ m.count i := by
  induction m using Quotient.inductionOn
  simp [List.prod_map_eq_pow_single i f hf]

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