English
The map toSyn is strictly monotone as a function between the relevant structures.
Русский
Переход toSyn является строго монотонным между соответствующими структурами.
LaTeX
$$$$ \\text{StrictMono}(m.toSyn). $$$$
Lean4
/-- Given `f : α →₀ ℕ`, `f.toMultiset` is the multiset with multiplicities given by the values of
`f` on the elements of `α`. We define this function as an `AddMonoidHom`.
Under the additional assumption of `[DecidableEq α]`, this is available as
`Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ)`; the two declarations are separate as this assumption
is only needed for one direction. -/
def toMultiset : (α →₀ ℕ) →+ Multiset α
where
toFun
f :=
Finsupp.sum f fun a n =>
n •
{ a }
-- Porting note: have to specify `h` or add a `dsimp only` before `sum_add_index'`.
-- see also: https://github.com/leanprover-community/mathlib4/issues/12129
map_add' _f _g := sum_add_index' (h := fun _ n => n • _) (fun _ ↦ zero_nsmul _) (fun _ ↦ add_nsmul _)
map_zero' := sum_zero_index
