A prime divisor of a geometric sum gives an order dividing the odd count
ProvedOddPerfectNumber.Kernel.geom_sum_dvd_order_dvd_odd_countfactorizationnumber-theoryperfect-numbers
Let p be a prime and q and e natural numbers. If p divides the sum of the first two e plus one powers of q, then the multiplicative order of q in the units modulo p divides two e plus one.
Preamble
import Mathlib
Formal statement
namespace OddPerfectNumber.Kernel
theorem geom_sum_dvd_order_dvd_odd_count {p q e : Nat} (hp : p.Prime)
(hdvd : Dvd.dvd p (∑ i ∈ Finset.range (2 * e + 1), q ^ i)) :
Dvd.dvd (orderOf (q : ZMod p)) (2 * e + 1) := by
sorry
end OddPerfectNumber.Kernel