Finset.mem_piAntidiagonal

theorem Finset.mem_piAntidiagonal : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ] [inst_3 : DecidableEq μ] {s : Finset ι} {n : μ} {f : ι →₀ μ}, f ∈ s.piAntidiagonal n ↔ f.support ⊆ s ∧ (f.sum fun x x => x) = n

This theorem states that a function `f` of type `ι →₀ μ` belongs to the antidiagonal set `piAntidiagonal s n` if and only if two conditions are met: Firstly, the support of the function `f` (the set of points where `f` does not vanish) must be a subset of the finite set `s`. Secondly, the sum of the function values of `f` over its support equals `n`. The types `ι` and `μ` are assumed to have decidable equality, with `μ` having an additional structure of a commutative monoid with an antidiagonal.

More concisely: A function `f` from a decidably-equaled set `ι` to a commutative monoid `μ` with an antidiagonal belongs to the antidiagonal set `piAntidiagonal s n` if and only if its support is a subset of `s` and the sum of its values over its support equals `n`.