Theorems · Theorem · number theory
Finset.Nat.antidiagonal_filter_fst_le_of_le
∀ {n k : ℕ},
k ≤ n →
{a ∈ Finset.HasAntidiagonal.antidiagonal n | a.1 ≤ k} =
Finset.map ((Function.Embedding.refl ℕ).prodMap { toFun := fun x => x + (n - k), inj' := ⋯ })
(Finset.HasAntidiagonal.antidiagonal k)- Defined in
- Mathlib.Data.Finset.NatAntidiagonal
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites19
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
- Equiv.symmproof · cited by 3,681
- add_commproof · cited by 1,535
- Finset.filterstatement and proof · cited by 949
- Finset.mapstatement and proof · cited by 747
- Finset.extproof · cited by 565
- Equiv.toEmbeddingproof · cited by 254
- Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218
- Equiv.prodCommproof · cited by 55
- add_left_injectivestatement and proof · cited by 49
- Finset.filter.congr_simpproof · cited by 47
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.