OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedFlagBudgetsCounts.lean
12 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.degreeBudget_leline 14 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.polynomial_degree_leline 23 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.occurrences_card_leline 33 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.fiber_card_leline 42 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.index_card_leline 51 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.representative_card_leline 63 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.degreeBudget_le_realline 70 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.polynomial_degree_le_realline 76 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.occurrences_card_le_realline 84 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.fiber_card_le_realline 90 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.index_card_le_realline 97 - theorem
OAI.Ostmann.Arithmetic.HistorySelectedFlagBudgets.representative_card_le_realline 105