Cullen numbers
DefinitionThe \(s\)-Cullen value#✓fully proved
MetaMathlibExt.sCullenNumber
For natural numbers \(s\) and \(n\), the \(s\)-Cullen value is \(C_{n,s} = n s^n + 1\).
def sCullenNumber (s n : ℕ) : ℕ := n * s ^ n + 1Sources
Sources
- Jon Grantham and Hester Graves, The abc Conjecture Implies That Only Finitely Many s-Cullen Numbers Are Repunits, Journal of Integer Sequences 24 (2021), https://cs.uwaterloo.ca/journals/JIS/VOL24/Grantham/gran4.tex.
Used by 1
Used by\(s\)-Cullen numbers
Definition\(s\)-Cullen numbers#✓fully proved
MetaMathlibExt.IsSCullenNumber
For natural numbers \(s\) and \(n\), write \(C_{n,s} = n s^n + 1\) for the \(s\)-Cullen value. A natural number \(m\) is an \(s\)-Cullen number when \(s \ge 2\) and \(m = C_{n,s}\) for some natural number \(n \ge 1\).
def IsSCullenNumber (s m : ℕ) : Prop :=
2 ≤ s ∧ ∃ n, 0 < n ∧ sCullenNumber s n = mdef sCullenNumber (s n : ℕ) : ℕ := n * s ^ n + 1MathlibExt/NumberTheory/SCullenNumber.lean:26
Uses 1
Statement usesThe \(s\)-Cullen value
2 fully proved
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.