prod_ofNatList — Mathlib

English

The product of the PrimeMultiset obtained from a list of naturals equals the product of the list.

Русский

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

LaTeX

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

Lean4

theorem prod_ofNatList (l : List ℕ) (h) : ((ofNatList l h).prod : ℕ) = l.prod :=
  by
  have := prod_ofNatMultiset (l : Multiset ℕ) h
  rw [Multiset.prod_coe] at this
  exact this

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