prod_nsmul — Mathlib

English

Let s be a multiset in a commutative monoid M and f a monoid homomorphism to N. Then (f on s).prod = f(s.prod).

Русский

Пусть s – мультимножество в коммутативном моноиде M, а f — моноидный гомоморфизм в N. Тогда prod(f(s)) = f(prod(s)).

LaTeX

$$$ (s.map f).prod = f\, s.prod $$$

Lean4

@[to_additive]
theorem prod_nsmul (m : Multiset M) : ∀ n : ℕ, (n • m).prod = m.prod ^ n
  | 0 => by
    rw [zero_nsmul, pow_zero]
    rfl
  | n + 1 => by rw [add_nsmul, one_nsmul, pow_add, pow_one, prod_add, prod_nsmul m n]

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