ofNatList — Mathlib

English

Lists of naturals can be turned into PrimeMultiset by first converting to a multiset and then lifting to primes.

Русский

Списки натуральных чисел можно преобразовать в PrimeMultiset через преобразование к мультимножества и последующее поднятие к простым.

LaTeX

$$$ \\operatorname{ofNatList}(l,h) = \\operatorname{ofNatMultiset}(\\operatorname{Multiset.ofList}(l),h) $$$$

Lean4

/-- Lists can be coerced to multisets; here we have some results
about how this interacts with our constructions on multisets. -/
def ofNatList (l : List ℕ) (h : ∀ p : ℕ, p ∈ l → p.Prime) : PrimeMultiset :=
  ofNatMultiset (l : Multiset ℕ) h

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