countP'_mul — Mathlib

English

The countP' function is additive over concatenation: countP'(p, l1 l2) = countP'(p, l1) + countP'(p, l2).

Русский

Подсчет countP' по конкатенации: countP'(p, l1 l2) = countP'(p, l1) + countP'(p, l2).

LaTeX

$$$\\operatorname{countP}'(p, l_{1} \\cdot l_{2}) = \\operatorname{countP}'(p, l_{1}) + \\operatorname{countP}'(p, l_{2}).$$$

Lean4

@[to_additive]
theorem countP'_mul (l₁ l₂ : FreeMonoid α) : (l₁ * l₂).countP' p = l₁.countP' p + l₂.countP' p :=
  by
  dsimp [countP']
  simp only [List.countP_append]

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