OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkUniversalPatternAggregationOriginalBasic.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryBulkUniversalPatternAggregation.blockDraw_sum_indicator_complex line 16
2. theorem OAI.Ostmann.Arithmetic.HistoryBulkUniversalPatternAggregation.original_block_sum_eq_biased_complex line 31
3. theorem OAI.Ostmann.Arithmetic.HistoryBulkUniversalPatternAggregation.sum_pattern_original_eq_patternComplexSum line 46