OAI/NumberTheory/Jacobsthal/Conclusions/Targets.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.NumberTheoryLean.Targets.representationCount line 18
2. def OAI.Erdos970.NumberTheoryLean.Targets.orderedRepresentations line 22
3. theorem OAI.Erdos970.NumberTheoryLean.Targets.representationCount_eq_card_orderedRepresentations line 27
4. def OAI.Erdos970.NumberTheoryLean.Targets.LogarithmicRepresentationLimit line 49
5. def OAI.Erdos970.NumberTheoryLean.Targets.AdditiveBasisPiLimit line 54
6. theorem OAI.Erdos970.NumberTheoryLean.Targets.public_limit_of_pi_limit line 59