OAI/NumberTheory/Jacobsthal/Probability/SourceMarkedStopping.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.tagFrom_none line 15
2. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.tagFrom_append_none line 23
3. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.terminal_cutoff_last line 33
4. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.terminal_lastD line 39
5. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.prefix_exponent_lower line 47
6. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.suffix_exponent_upper line 65
7. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.no_candidate_below_search line 75
8. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixTools.sourceTag_prefix_eq line 89
9. theorem OAI.Erdos970.NumberTheoryLean.MarkedPrefixCandidate.marked_prefix_candidate line 111
10. theorem OAI.Erdos970.NumberTheoryLean.SourceMarkedStopping.marked_prefix_forces_actual_stop line 239