Theorems · Definition · combinatorics
Finset.piAntidiag
{ι : 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 n.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Pi
- Cited by
- 19 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Equivproof · cited by 8,337
- Finset.cardproof · cited by 2,327
- Finset.mapproof · cited by 747
- Finset.HasAntidiagonalstatement and proof · cited by 48
- Trunc.liftproof · cited by 5
- Fintype.truncEquivFinOfCardEqproof · cited by 2
- Finset.finAntidiagonalproof · cited by 1
Cited by20
Results whose statement or proof uses this declaration.
- Finset.finsuppAntidiagproof · cited by 25
- Finset.pairwiseDisjoint_piAntidiag_map_addRightEmbeddingstatement and proof · cited by 3
- Finset.piAntidiag_consstatement · cited by 2
- Finset.piAntidiag_empty_of_ne_zerostatement · cited by 2
- Finset.piAntidiag_zerostatement · cited by 2
- Finset.nsmul_piAntidiagstatement · cited by 2
- Finset.mem_finsuppAntidiagproof · cited by 2
- Finset.mem_piAntidiagstatement · cited by 1
- Finset.piAntidiag_empty_zerostatement · cited by 1
- Finset.map_nsmul_piAntidiagstatement and proof · cited by 1
- Finset.sum_pow_eq_sum_piAntidiag_of_commutestatement and proof · cited by 1
- Finset.finsuppAntidiag_zeroproof · cited by 0