Main results
The main results that the formalization.yaml of FormalFrontier/sequence-growth lists under status.main_results at commit ccf81c71, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.
| Declaration | Kind | Where | Note |
|---|---|---|---|
Nat.DivisionGrowth.affine_lower_bound |
theorem | SequenceGrowth/Data/Nat/DivisionGrowth.lean, line 71 | Sorry count 0. |
Nat.DivisionGrowth.eventually_dominates |
theorem | SequenceGrowth/Data/Nat/DivisionGrowth.lean, line 99 | Sorry count 0. |
Quoted from the main results in formalization.yaml of FormalFrontier/sequence-growth at commit ccf81c71, Apache-2.0.
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.