prod_ofPNatMultiset — Mathlib

English

The product of a Prime Multiset formed from naturals equals the product of the original Nat multiset when viewed as PNats.

Русский

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

LaTeX

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

Lean4

theorem prod_ofPNatMultiset (v : Multiset ℕ+) (h) : ((ofPNatMultiset v h).prod : ℕ+) = v.prod :=
  by
  dsimp [prod]
  rw [to_ofPNatMultiset]

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