count_replicate — Mathlib

English

For all a,b and n ∈ ℕ, the multiplicity of a in the multiset obtained by replicating b n times equals n if a = b and 0 otherwise.

Русский

Для любых a, b и n ∈ ℕ кратность элемента a в мультиcете, полученном повторением b n раз, равна n если a = b и 0 в противном случае.

LaTeX

$$$$ \\operatorname{count}(a, \\operatorname{replicate}(n,b)) = \\begin{cases} n & a=b \\\\ 0 & a \\neq b \\end{cases} $$$$

Lean4

theorem count_replicate (a b : α) (n : ℕ) : count a (replicate n b) = if b = a then n else 0 :=
  by
  convert List.count_replicate (a := a)
  · rw [← coe_count, coe_replicate]
  · simp

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