coeNatMonoidHom — Mathlib

English

The coercion to naturals extends to a monoid hom from PrimeMultiset to Multiset ℕ.

Русский

Вложение в множества чисел натурального образует единообразный гомоморф моноидов.

LaTeX

$$coeNatMonoidHom : PrimeMultiset →+ Multiset ℕ$$

Lean4

/-- `PrimeMultiset.coe`, the coercion from a multiset of primes to a multiset of
naturals, promoted to an `AddMonoidHom`. -/
def coeNatMonoidHom : PrimeMultiset →+ Multiset ℕ :=
  Multiset.mapAddMonoidHom (↑)

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