OAI/NumberTheory/Ostmann/Supply/CompletionArithmetic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Supply.CompletionCounting.multiplesUpTo line 8
2. theorem OAI.Ostmann.Supply.CompletionCounting.card_multiplesUpTo line 10
3. theorem OAI.Ostmann.Supply.CompletionCounting.card_multiplesUpTo_le line 15
4. theorem OAI.Ostmann.Supply.CompletionCounting.sum_inverse_sq_le line 20
5. theorem OAI.Ostmann.Supply.CompletionCounting.card_dvd_union_le line 40
6. theorem OAI.Ostmann.Supply.CompletionCounting.card_nonsquarefree_le line 49
7. theorem OAI.Ostmann.Supply.CompletionCounting.card_noncoprime_le line 71