toDFinsupp_replicate

Mathlib.Data.DFinsupp.Multiset

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

← MathLib Explorer

English

toDFinsupp( Multiset.replicate n a ) = DFinsupp.single a n.

Русский

toDFinsupp( Multiset.replicate n a ) = DFinsupp.single a n.

LaTeX

$$$$ \\operatorname{toDFinsupp}\\left( \\operatorname{Multiset.replicate} n\\, a \\right) = \\operatorname{DFinsupp.single} a\\, n $$$$

Lean4

@[simp]
theorem toDFinsupp_replicate (a : α) (n : ℕ) : toDFinsupp (Multiset.replicate n a) = DFinsupp.single a n :=
  by
  ext i
  dsimp [toDFinsupp]
  simp [count_replicate]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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