cardHom — Mathlib

English

The cardHom is the natural homomorphism sending a multiset to its cardinality; it is additive: card(s + t) = card s + card t.

Русский

cardHom — естественная гомоморфная карта, отправляющая мультимножество в его кардинал; она аддитивна: card(s + t) = card s + card t.

LaTeX

$$$ \operatorname{cardHom}(s+t) = \operatorname{card}(s) + \operatorname{card}(t) $$$

Lean4

/-- `Multiset.card` bundled as a group hom. -/
@[simps]
def cardHom : Multiset α →+ ℕ where
  toFun := card
  map_zero' := card_zero
  map_add' := card_add

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