Theorems · Theorem · combinatorics
Finset.mapRange_finsuppAntidiag_subset
∀ {ι : Type u_1} {μ : Type u_2} {μ' : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ]
[inst_2 : Finset.HasAntidiagonal μ] [inst_3 : DecidableEq μ] [inst_4 : AddCommMonoid μ']
[inst_5 : Finset.HasAntidiagonal μ'] [inst_6 : DecidableEq μ'] {e : μ ≃+ μ'} {s : Finset ι} {n : μ},
Finset.map (Finsupp.mapRange.addEquiv e).toEmbedding (s.finsuppAntidiag n) ⊆ s.finsuppAntidiag (e n)- Defined in
- Mathlib.Algebra.Order.Antidiag.Finsupp
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites20
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coestatement and proof · cited by 62,936
- Finsetstatement and proof · cited by 13,712
- AddCommMonoidstatement and proof · cited by 12,281
- Finsuppstatement and proof · cited by 5,255
- AddEquivstatement and proof · cited by 1,087
- Finsupp.supportproof · cited by 828
- Finset.mapstatement · cited by 747
- Finsupp.sumproof · cited by 481
- Equiv.toEmbeddingstatement and proof · cited by 254
- AddEquiv.toEquivstatement and proof · cited by 174
- EquivLike.toEquivproof · cited by 125
- subset_transproof · cited by 63
Cited by1
Results whose statement or proof uses this declaration.
- Finset.mapRange_finsuppAntidiag_eqproof · cited by 1