Theorems · Definition · number theory
Nat.finMulAntidiag
(d : ℕ) → ℕ → Finset (Fin d → ℕ)
The Finset of all d-tuples of natural numbers whose product is n. Defined to be ∅ when
n = 0.
- Defined in
- Mathlib.Algebra.Order.Antidiag.Nat
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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 · cited by 13,712
- Finset.mapproof · cited by 747
- Equiv.toEmbeddingproof · cited by 254
- PNat.valproof · cited by 226
- Additive.ofMulproof · cited by 155
- Additive.toMulproof · cited by 109
- Function.Embedding.transproof · cited by 83
- Function.Embedding.arrowCongrRightproof · cited by 3
- PNat.coe_injectiveproof · cited by 3
- Finset.finAntidiagonalproof · cited by 1
Cited by13
Results whose statement or proof uses this declaration.
- Nat.mem_finMulAntidiagstatement · cited by 7
- Nat.dvd_of_mem_finMulAntidiagstatement and proof · cited by 3
- Nat.card_finMulAntidiag_of_squarefreestatement · cited by 1
- Nat.prod_eq_of_mem_finMulAntidiagstatement and proof · cited by 1
- Nat.image_apply_finMulAntidiagstatement and proof · cited by 0
- Nat.image_piFinTwoEquiv_finMulAntidiagstatement and proof · cited by 0
- Nat.finMulAntidiag_eq_piFinset_divisors_filterstatement and proof · cited by 0
- Nat.finMulAntidiag_existsUnique_prime_dvdstatement and proof · cited by 0
- Nat.finMulAntidiag_onestatement · cited by 0
- Nat.finMulAntidiag_threestatement and proof · cited by 0
- Nat.finMulAntidiag_zero_rightstatement · cited by 0
- Nat.finMulAntidiag_zero_leftstatement · cited by 0