prod_map_mul — Mathlib

English

For any multiset m in a commutative monoid M, and any natural n, the product of n-fold sum of m equals the n-th power of m.prod: (n • m).prod = (m.prod)^n.

Русский

Для любого мультимножества m в коммутативном моноиде M и любого натурального n, произведение n-разового сложения m равно n-й степени prod(m).

LaTeX

$$$ (n \cdot m).prod = (m.prod)^{n} $$$

Lean4

@[to_additive (attr := simp)]
theorem prod_map_mul : (m.map fun i => f i * g i).prod = (m.map f).prod * (m.map g).prod :=
  m.prod_hom₂ (· * ·) mul_mul_mul_comm (mul_one _) _ _

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