Theorems · Definition · combinatorics
Finset.finsuppAntidiag
{ι : Type u_1} →
{μ : Type u_2} →
[DecidableEq ι] →
[inst : AddCommMonoid μ] → [Finset.HasAntidiagonal μ] → [DecidableEq μ] → Finset ι → μ → Finset (ι →₀ μ)The finset of functions ι →₀ μ with support contained in s and sum equal to n.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Finsupp
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finsuppstatement · cited by 5,255
- Finset.filterproof · cited by 949
- Finset.mapproof · cited by 747
- Finset.attachproof · cited by 168
- Finset.HasAntidiagonalstatement and proof · cited by 48
- Finset.piAntidiagproof · cited by 19
Cited by27
Results whose statement or proof uses this declaration.
- Nat.Partition.hasProd_genFunproof · cited by 4
- Finset.finsuppAntidiagEquivstatement · cited by 4
- MvPowerSeries.coeff_prodstatement and proof · cited by 3
- Finset.finsuppAntidiagEquivSubtypestatement and proof · cited by 2
- Finset.mem_finsuppAntidiagstatement · cited by 2
- MvPowerSeries.coeff_eq_zero_of_constantCoeff_nilpotentproof · cited by 2
- PowerSeries.coeff_prodstatement and proof · cited by 2
- Finset.mapRange_finsuppAntidiag_eqstatement and proof · cited by 1
- Finset.mapRange_finsuppAntidiag_subsetstatement · cited by 1
- Finset.finsuppAntidiagEquivSubtype_apply_coestatement and proof · cited by 1
- Finset.mem_finsuppAntidiag_insertstatement · cited by 1
- MvPowerSeries.truncTotal_subst_eq_truncTotal_subst_truncTotal_of_leproof · cited by 1