Bennett sum divisible in subring

Proved

D1Bound5.bennett_sum_divisible_in_subring

by tp · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

diophantine-tuplesnumber-theory

A finite sum of multiples whose quotients lie in a fixed subring has a quotient in that same subring. The divisor itself need not belong to it.

Preamble

import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Combinatorics.Enumerative.Catalan.Basic
import Mathlib.RingTheory.Binomial
import Mathlib.Tactic.LinearCombination
import Mathlib.Tactic.NormNum

Formal statement

section
open Finset

namespace D1Bound5


theorem _root_.D1Bound5.bennett_sum_divisible_in_subring
    {F T : Type*} [CommRing F] (S : Subring F) (s : Finset T)
    (x : T → F) (d : F)
    (h : ∀ t ∈ s, ∃ q ∈ S, x t = d * q) :
    ∃ q ∈ S, ∑ t ∈ s, x t = d * q := by sorry



end D1Bound5
end

Source

D1Bound5/BennettSubringSums.lean, lines 7-25, SHA-256 5c21c49f96a2c66d645b20532b67dda8cde35833f4e0f3fe6b545b7454d81ecf. Project: https://github.com/tomislav-math/d1-bound5-lean

View graph