prod_const — Mathlib

English

Let m be a Multiset, s a Finset, hs: m.toFinset ⊆ s; then m.prod = ∏ i ∈ s, i^{m.count i}.

Русский

Пусть m — мультисет, s — Finset, hs: m.toFinset ⊆ s; тогда m.prod = ∏ i ∈ s, i^{m.count i}.

LaTeX

$$$\displaystyle m.prod = \prod i \in s, i^{\mathrm{count}(i,m)}$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_const (b : M) : ∏ _x ∈ s, b = b ^ #s :=
  (congr_arg _ <| s.val.map_const b).trans <| Multiset.prod_replicate (#s) b

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