OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedFlagBudgets.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.selectedExponent line 13
2. theorem OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.selectedExponent_pos line 16
3. theorem OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.count_exp_le_selected line 24
4. theorem OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.selected_flag_budgets_eventually line 37