Theorems · Theorem · number theory

Nat.divisors_eq_map_attach_Iic_factorization_prod_pow

∀ {n : ℕ},
  n ≠ 0 →
    n.divisors =
      Finset.map { toFun := fun x => (↑x).prod fun x1 x2 => x1 ^ x2, inj' := ⋯ } (Finset.Iic n.factorization).attach

Defined in: Mathlib.Data.Nat.Factorization.Divisors
Cited by: 0 results in Mathlib
Foundations: Depth 97 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

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
Finsuppstatement and proof · cited by 5,255
Finset.imageproof · cited by 910
Finset.mapstatement · cited by 747
Finset.Iicstatement and proof · cited by 280
Finsupp.prodstatement and proof · cited by 231
Nat.factorizationstatement and proof · cited by 215
Finset.attachstatement and proof · cited by 168
Nat.divisorsstatement and proof · cited by 137
Finset.map_eq_imageproof · cited by 50
Finset.image_imageproof · cited by 16
Finset.attach_image_valproof · cited by 6

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.