Trivial nil sublist and unit product of empty sequence

Proved

Erdos390.tail_divisor_nil_sublist

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

combinatoricsorder-theory

Let $L$ be a list of natural numbers. The empty list $[]$ is a sublist of $L$ (List.Sublist [] L), and its product is unity (List.prod [] = 1).

Preamble

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

Formal statement

namespace Erdos390

theorem tail_divisor_nil_sublist
    (L : List ℕ) :
    List.Sublist [] L ∧ List.prod [] = 1 := by sorry

end Erdos390

Source

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