countP — Mathlib

English

countP is a bundled monoid homomorphism sending a word to the multiplicative natural number equal to the additive count of p in that word.

Русский

countP — это связанный гомоморфизм моноида, переводящий слово в мультипликативноеNat, равное аддитивному countP'(p, слово).

LaTeX

$$$\\text{countP}: FreeMonoid α \\to^* \\mathrm{Multiplicative} \\mathbb{N},\\quad \\text{toFun}(l) = \\mathrm{Multiplicative}.ofAdd(\\operatorname{countP}'(p, l)).$$$

Lean4

/-- `List.countP` as a bundled additive monoid homomorphism. -/
def countP : FreeAddMonoid α →+ ℕ where
  toFun := FreeAddMonoid.countP' p
  map_zero' := countP'_zero p
  map_add' := countP'_add p

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