count — Mathlib

English

The operation count x on a word l counts the occurrences of x in l; it is the coefficient of x in l.

Русский

Операция count x на слове l подсчитывает число вхождений x в l; это коэффициент x в l.

LaTeX

$$$\\text{count}(x)(l) = \\text{List.count}(x, l.\\mathrm{toList})$$$

Lean4

/-- `List.count` as a bundled additive monoid homomorphism. -/
def count [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ :=
  countP (· = x)

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