Prove2Me

Tail quotient subset from complement divisor subset

Proved
Erdos390.tail_from_complement_divisor

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

algebracombinatoricsnumber-theory

Let n,h,D∈Nn, h, D \in \mathbb{N} and let C⊆(2n,2n+h]C \subseteq (2n, 2n + h] be a finite subset such that ∏c∈Cc=D\prod_{c \in C} c = D. Then the set difference tail=(2n,2n+h]∖C\mathrm{tail} = (2n, 2n + h] \setminus C satisfies:

tail⊆(2n,2n+h]and(∏a∈taila)⋅D=∏k∈(2n,2n+h]k.\mathrm{tail} \subseteq (2n, 2n + h] \quad \text{and} \quad \left(\prod_{a \in \mathrm{tail}} a\right) \cdot D = \prod_{k \in (2n, 2n + h]} k.
Preamble
import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390
Formal statement
namespace Erdos390

theorem tail_from_complement_divisor
    {n h D : ℕ} {C : Finset ℕ}
    (hC_sub : C ⊆ factorInterval (2 * n) (2 * n + h))
    (hC_prod : C.prod id = D) :
    ∃ tail : Finset ℕ,
      tail ⊆ factorInterval (2 * n) (2 * n + h) ∧
      tail.prod id * D = (factorInterval (2 * n) (2 * n + h)).prod id := by sorry

end Erdos390
Source
P. Erdős, Some problems in number theory, 1975; Erdős Problem 390 tail complement divisor inversion

View graph