count — Mathlib

English

countP is a bundled additive monoid homomorphism from FreeAddMonoid α to ℕ, sending l to FreeAddMonoid.countP' p l.

Русский

countP — это связанный аддитивный моноид-гомоморфизм от FreeAddMonoid α к ℕ, отправляющий l в FreeAddMonoid.countP' p l.

LaTeX

$$$\\text{countP} : FreeAddMonoid α \\to^+ \\mathbb{N},\\quad \\text{toFun}(l) = \\operatorname{countP}'(p, l).$$$

Lean4

/-- `List.count` as a bundled additive monoid homomorphism. -/
-- Porting note: was (x = ·)

def count [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ :=
  countP (· = x)

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