OAI/NumberTheory/Jacobsthal/Conclusions/IteratedLogModel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.Targets.JacobsthalIteratedLog line 9

    Source documentation

    The strengthened main theorem of Manuscript 293, revision ad16712e. The interval, prime-factor and translation quantifiers are unchanged.

    Also declared: ComparatorChallenges/JacobsthalImproved.lean:13 (same declaration text).

    def JacobsthalIteratedLog : Prop :=
    …