Theorems · Definition · combinatorics
Finset.HasAntidiagonal.antidiagonal
{A : Type u_1} → {inst : AddMonoid A} → [self : Finset.HasAntidiagonal A] → A → Finset (A × A)The antidiagonal of an element n is the finset of pairs (i, j) such that
i + j = n.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Prod
- Cited by
- 218 results in Mathlib
- Foundations
- Depth 2 from the axioms, rests on 5 definitions · uses no axioms
- Assumes
- Finset.HasAntidiagonal
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- AddMonoidstatement and proof · cited by 2,864
- Finset.HasAntidiagonalstatement and proof · cited by 48
Cited by231
Results whose statement or proof uses this declaration.
- Finset.HasAntidiagonal.mem_antidiagonalstatement · cited by 51
- Polynomial.homogenizeproof · cited by 30
- PowerSeries.coeff_mulstatement and proof · cited by 29
- Polynomial.coeff_mulstatement and proof · cited by 29
- MvPowerSeries.coeff_mulstatement and proof · cited by 22
- Finset.Nat.sum_antidiagonal_eq_sum_range_succstatement · cited by 15
- Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mkstatement · cited by 14
- MvPolynomial.coeff_mulstatement and proof · cited by 10
- BinaryTree.treesOfNumNodesEqproof · cited by 10
- MonomialOrder.degree_mul_leproof · cited by 10
- Polynomial.coeff_mul_X_powproof · cited by 9
- Finset.HasAntidiagonal.antidiagonal_zerostatement · cited by 8
Showing the 200 most cited of 231.