English
Antidiagonal' assigns to f a finitely supported function on pairs of finitely supported functions, encoding all pairs that sum to f.
Русский
Антидиагональ' присваивает $f$ тоффуобразующуюся функцию на пары функций, кодируя все пары, чьи суммы дают $f$.
LaTeX
$$def\\ antidiagonal'(f) = \\operatorname{Multiset}.toFinsupp\\left( (\\mathrm{Finsupp}.toMultiset f).antidiagonal.map (\\mathrm{Prod.map} \\mathrm{Multiset}.toFinsupp \\mathrm{Multiset}.toFinsupp) \\right)$$
Lean4
/-- The `Finsupp` counterpart of `Multiset.antidiagonal`: the antidiagonal of
`s : α →₀ ℕ` consists of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ + t₂ = s`.
The finitely supported function `antidiagonal s` is equal to the multiplicities of these pairs. -/
def antidiagonal' (f : α →₀ ℕ) : (α →₀ ℕ) × (α →₀ ℕ) →₀ ℕ :=
Multiset.toFinsupp ((Finsupp.toMultiset f).antidiagonal.map (Prod.map Multiset.toFinsupp Multiset.toFinsupp))
