val_replicate

Mathlib.Data.Sym.Basic

URI: https://scilib.ai/kg/mathlib#Sym.val_replicate

English

The underlying value of replicate n a equals Multiset.replicate n a.

Русский

Основание replicate n a равно Multiset.replicate n a.

LaTeX

$$$ (\mathrm{replicate}(n,a)).\text{val} = \mathrm{Multiset.replicate}(n,a). $$$

Lean4

theorem val_replicate : (replicate n a).val = Multiset.replicate n a := by rw [val_eq_coe, coe_replicate]

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

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

Разделы

Аффилиация

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