Theorems · Definition · number theory
Int.divisorsAntidiag
ℤ → Finset (ℤ × ℤ)
Pairs of divisors of an integer as a finset.
z.divisorsAntidiag is the finset of pairs (a, b) : ℤ × ℤ such that a * b = z.
By convention, we set Int.divisorsAntidiag 0 = ∅.
O(|z|). Computed from Nat.divisorsAntidiagonal.
- Defined in
- Mathlib.NumberTheory.Divisors
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 62 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 and proof · cited by 13,712
- Finset.mapproof · cited by 747
- Equiv.toEmbeddingproof · cited by 254
- Function.Embedding.transproof · cited by 83
- Nat.divisorsAntidiagonalproof · cited by 61
- Finset.disjUnionproof · cited by 55
- Equiv.negproof · cited by 53
- Nat.castEmbeddingproof · cited by 29
- Function.Embedding.prodMapproof · cited by 23
Cited by17
Results whose statement or proof uses this declaration.
- Int.mem_divisorsAntidiagstatement · cited by 0
- Int.neg_mem_divisorsAntidiagstatement · cited by 0
- Int.swap_mem_divisorsAntidiagstatement · cited by 0
- Int.divisorsAntidiag_natCaststatement · cited by 0
- Int.divisorsAntidiag_negstatement · cited by 0
- Int.divisorsAntidiag_neg_natCaststatement and proof · cited by 0
- Int.divisorsAntidiag_ofNatstatement · cited by 0
- Int.divisorsAntidiag_zerostatement · cited by 0
- Int.divisorsAntidiagonal_fourstatement · cited by 0
- Int.divisorsAntidiagonal_onestatement · cited by 0
- Int.divisorsAntidiagonal_threestatement · cited by 0
- Int.divisorsAntidiagonal_twostatement · cited by 0