prod_pow_eq_pow_sum — Mathlib

English

Let s be a finite set and a be an element of a monoid. The product over s of a raised to f(i) equals a raised to the sum over i in s of f(i).

Русский

Пусть s конечен и a лежит в моноиде. Произведение по i∈s a^{f(i)} равно a^{∑_{i∈s} f(i)}.

LaTeX

$$$\\prod_{i \\in s} a^{f(i)} = a^{\\sum_{i \\in s} f(i)}$$$

Lean4

@[to_additive sum_nsmul_assoc]
theorem prod_pow_eq_pow_sum (s : Finset ι) (f : ι → ℕ) (a : M) : ∏ i ∈ s, a ^ f i = a ^ ∑ i ∈ s, f i :=
  cons_induction (by simp) (fun _ _ _ _ ↦ by simp [prod_cons, sum_cons, pow_add, *]) s

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