Tail divisor subset from duplicate-free factor list

Proved

Erdos390.tail_divisor_from_nodup_list

by doctosil · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

algebracombinatoricsnumber-theory

Let $n, h, D \in \mathbb{N}$ and let $l$ be a duplicate-free list (l.Nodup) of integers in $(2n, 2n + h]$ whose product equals $D$ . Then the finite set $C = l.\mathrm{toFinset}$ satisfies:

C \subseteq (2n, 2n + h] \quad \text{and} \quad \prod_{c \in C} c = D.

Preamble

import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_divisor_from_nodup_list
    {n h D : ℕ} (l : List ℕ)
    (hsub : ∀ x ∈ l, x ∈ factorInterval (2 * n) (2 * n + h))
    (hnodup : l.Nodup)
    (hprod : l.prod = D) :
    ∃ C : Finset ℕ,
      C ⊆ factorInterval (2 * n) (2 * n + h) ∧
      C.prod id = D := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Erdős Problem 390 tail divisor subset from list

View graph