Singleton sublist inclusion and factor evaluation

Proved

Erdos390.tail_divisor_singleton_sublist

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

combinatoricsorder-theory

Let $L$ be a list of natural numbers and let $x \in \mathbb{N}$ satisfy $x \in L$ . Then the singleton list $[x]$ is a sublist of $L$ (List.Sublist [x] L), and its product is identically $x$ (List.prod [x] = x).

Preamble

import Mathlib.Data.List.Basic
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_divisor_singleton_sublist
    {L : List ℕ} {x : ℕ}
    (hx : x ∈ L) :
    List.Sublist [x] L ∧ List.prod [x] = x := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Mathlib List.singleton_sublist

View graph