prod_ofPNatList — Mathlib

English

The product of the PrimeMultiset formed from a list of positive naturals equals the list product.

Русский

Произведение мультимножества простых, полученного из списка положительных натуральных чисел, равно произведению списка.

LaTeX

$$$ \\operatorname{prod}(\\operatorname{ofPNatList}(l,h)) = \\operatorname{prod}(l) $$$

Lean4

theorem prod_ofPNatList (l : List ℕ+) (h) : (ofPNatList l h).prod = l.prod :=
  by
  have := prod_ofPNatMultiset (l : Multiset ℕ+) h
  rw [Multiset.prod_coe] at this
  exact this

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