Vanishing off the index set of a function antidiagonal #
Finset.piAntidiag s n is the finset of functions with support contained in s whose values sum
to n over s. Such a function therefore vanishes at every point outside s.
Main results #
Finset.eq_zero_of_notMem_of_mem_piAntidiag: a member ofFinset.piAntidiag s nvanishes offs.
theorem
Finset.eq_zero_of_notMem_of_mem_piAntidiag
{ι : Type u_1}
{μ : Type u_2}
[DecidableEq ι]
[AddCommMonoid μ]
[HasAntidiagonal μ]
[DecidableEq μ]
{s : Finset ι}
{n : μ}
{f : ι → μ}
{i : ι}
(hi : i ∉ s)
(hf : f ∈ s.piAntidiag n)
:
A function in Finset.piAntidiag s n has support contained in s, so it takes the value 0
at every point outside s.