coeNat_factorMultiset — Mathlib

English

The natural-coercion of the factor multiset equals the prime factor multiset of the number.

Русский

Соотношение фактормультимножества и натурального множителя числа через соответствие факторов.

LaTeX

$$$ (factorMultiset n : \\operatorname{Multiset}\\mathbb{N}) = (Nat.primeFactorsList n : \\operatorname{Multiset}\\mathbb{N}) $$$

Lean4

theorem coeNat_factorMultiset (n : ℕ+) : (factorMultiset n : Multiset ℕ) = (Nat.primeFactorsList n : Multiset ℕ) :=
  PrimeMultiset.to_ofNatMultiset (Nat.primeFactorsList n) (@Nat.prime_of_mem_primeFactorsList n)

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