coe_fill — Mathlib

English

The count of a particular element in a filled Sym term corresponds to the added copies in the fill operation.

Русский

Количество данного элемента в заполненном Sym-терме соответствует добавленным копиям в операции fill.

LaTeX

$$$\\text{count}_{a}(\\mathrm{fill}\\ a\\ i\\ s) = i$ if $a$ equals the filled element; otherwise the count remains unchanged.$$

Lean4

theorem coe_fill {a : α} {i : Fin (n + 1)} {m : Sym α (n - i)} : (fill a i m : Multiset α) = m + replicate i a :=
  rfl

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