factorMultiset_one — Mathlib

English

Factoring a number to a multiset of primes yields zero when mapped to the additive monoid.

Русский

Факторизация числа в мультимножество простых складывается в нуль в аддитивном моноиде.

LaTeX

$$$ factorMultiset\\ 1 = 0 $$$

Lean4

/-- Factoring gives a homomorphism from the multiplicative
monoid ℕ+ to the additive monoid of multisets. -/
theorem factorMultiset_one : factorMultiset 1 = 0 := by
  simp [factorMultiset, PrimeMultiset.ofNatList, PrimeMultiset.ofNatMultiset]

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