replicate — Mathlib

English

Define replicate(n,a) as the element of Sym α n whose underlying multiset is the n-fold replicate of a.

Русский

Задаём replicate(n,a) как элемент Sym α n, чьё основание — мультсет, повторяющий a n раз.

LaTeX

$$$ \mathrm{replicate}(n,a) = \langle \mathrm{Multiset.replicate}(n,a), \mathrm{card\_replicate}\,\rangle. $$$

Lean4

/-- `replicate n a` is the sym containing only `a` with multiplicity `n`. -/
def replicate (n : ℕ) (a : α) : Sym α n :=
  ⟨Multiset.replicate n a, Multiset.card_replicate _ _⟩

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