prod_ofNatMultiset — Mathlib

English

The product of the PrimeMultiset obtained from a Nat multiset equals the product of the Nat multiset.

Русский

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

LaTeX

$$$ ((\\operatorname{ofNatMultiset}(v,h)).prod : \\mathbb{N}) = (v.prod : \\mathbb{N}) $$$

Lean4

theorem prod_ofNatMultiset (v : Multiset ℕ) (h) : ((ofNatMultiset v h).prod : ℕ) = (v.prod : ℕ) := by
  rw [coe_prod, to_ofNatMultiset]

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