coe_prod — Mathlib

English

For a prime multiset v, the natural product of v (as a natural) equals the product of the underlying naturals multiset.

Русский

Для мультимножества простых v естественный произведение v равно произведению соответствующего мультимножества натуральных чисел.

LaTeX

$$$ \\bigl(v \\operatorname{prod}\\bigr) = \\bigl(v \\text{ viewed as } \\operatorname{Multiset}(\\mathbb{N})\\bigr).\\mathrm{prod} $$$

Lean4

theorem coe_prod (v : PrimeMultiset) : (v.prod : ℕ) = (v : Multiset ℕ).prod :=
  by
  have h : (v.prod : ℕ) = ((v.map (↑) : Multiset ℕ+).map (↑)).prod :=
    PNat.coeMonoidHom.map_multiset_prod v.toPNatMultiset
  simpa [Multiset.map_map] using h

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