OAI/NumberTheory/Ostmann/Arithmetic/HistorySelectedPatternFlagErrorCounts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.patternCount line 18
2. theorem OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.patternCount_pos line 20
3. theorem OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.pattern_card_le line 24
4. theorem OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.pattern_card_le_real line 34
5. def OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.patternLogCost line 38
6. theorem OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.patternLogCost_nonneg line 40
7. theorem OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.patternCount_cast_eq_exp line 45
8. theorem OAI.Ostmann.Arithmetic.HistorySelectedPatternFlagError.pattern_card_le_exp line 53