replicate

Mathlib.Data.Multiset.Replicate

URI: https://scilib.ai/kg/mathlib#Multiset.replicate

English

The multiset replicate(n,a) is the multiset containing a with multiplicity n.

Русский

Множество replicate(n,a) состоит из элемента a с кратностью n.

LaTeX

$$$\\operatorname{replicate}(n,a) = \\operatorname{Multiset.ofList}(\\operatorname{List.replicate}(n,a))$$$

Lean4

/-- `replicate n a` is the multiset containing only `a` with multiplicity `n`. -/
def replicate (n : ℕ) (a : α) : Multiset α :=
  List.replicate n a

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru