toMultiset_single — Mathlib

English

For any a and n, toMultiset( DFinsupp.single a n ) equals Multiset.replicate n a.

Русский

Для любого элемента a и числа n выполнено toMultiset( DFinsupp.single a n ) = Multiset.replicate n a.

LaTeX

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

Lean4

@[simp]
theorem toMultiset_single (a : α) (n : ℕ) : toMultiset (DFinsupp.single a n) = Multiset.replicate n a :=
  DFinsupp.sumAddHom_single _ _ _

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