Results about divisors and factorizations

theorem Nat.coe_divisors_eq_prod_pow_le_factorization {n : ℕ} (hn : n ≠ 0) : ↑n.divisors = {x : ℕ | ∃ f ≤ n.factorization, (f.prod fun (x1 x2 : ℕ) => x1 ^ x2) = x}

theorem Nat.divisors_eq_image_Iic_factorization_prod_pow {n : ℕ} (hn : n ≠ 0) : n.divisors = Finset.image (fun (x : ℕ →₀ ℕ) => x.prod fun (x1 x2 : ℕ) => x1 ^ x2) (Finset.Iic n.factorization)

theorem Nat.Iic_factorization_prod_pow_injective (n : ℕ) : Function.Injective fun (x : ↥(Finset.Iic n.factorization)) => (↑x).prod fun (x1 x2 : ℕ) => x1 ^ x2

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

theorem Nat.coe_properDivisors_eq_prod_pow_lt_factorization {n : ℕ} : ↑n.properDivisors = {x : ℕ | ∃ f < n.factorization, (f.prod fun (x1 x2 : ℕ) => x1 ^ x2) = x}

theorem Nat.properDivisors_eq_image_Iio_factorization_prod_pow {n : ℕ} : n.properDivisors = Finset.image (fun (x : ℕ →₀ ℕ) => x.prod fun (x1 x2 : ℕ) => x1 ^ x2) (Finset.Iio n.factorization)

theorem Nat.Iio_factorization_prod_pow_injective (n : ℕ) : Function.Injective fun (x : ↥(Finset.Iio n.factorization)) => (↑x).prod fun (x1 x2 : ℕ) => x1 ^ x2

theorem Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow {n : ℕ} : n.properDivisors = Finset.map { toFun := fun (x : ↥(Finset.Iio n.factorization)) => (↑x).prod fun (x1 x2 : ℕ) => x1 ^ x2, inj' := ⋯ } (Finset.Iio n.factorization).attach