Theorems · Theorem · number theory
Nat.divisorsAntidiagonal_eq_prod_filter_of_le
∀ {n N : ℕ}, n ≠ 0 → n ≤ N → n.divisorsAntidiagonal = {x ∈ Finset.Ioc 0 N ×ˢ Finset.Ioc 0 N | x.1 * x.2 = n}Useful lemma for reordering sums.
- Defined in
- Mathlib.NumberTheory.Divisors
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 66 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Finsetstatement · cited by 13,712
- le_reflproof · cited by 2,061
- SProd.sprodstatement and proof · cited by 1,750
- Finset.filterstatement and proof · cited by 949
- le_imp_le_of_le_of_leproof · cited by 576
- Finset.extproof · cited by 565
- Finset.Iocstatement and proof · cited by 301
- Nat.divisorsAntidiagonalstatement · cited by 61
- Nat.mem_divisorsAntidiagonalproof · cited by 11
Cited by1
Results whose statement or proof uses this declaration.
- ArithmeticFunction.sum_Ioc_mul_eq_sum_prod_filterproof · cited by 1