OAI/NumberTheory/OrdinaryCorrelations/AbsoluteDefect/SmoothPart.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinarySmoothRough.smoothPart line 21
2. def OAI.OrdinarySmoothRough.roughPart line 24
3. lemma OAI.OrdinarySmoothRough.parts_mul line 27
4. lemma OAI.OrdinarySmoothRough.parts_coprime line 32
5. lemma OAI.OrdinarySmoothRough.smoothPart_mem line 44
6. lemma OAI.OrdinarySmoothRough.roughPart_coprime_prime line 62
7. lemma OAI.OrdinarySmoothRough.roughPart_coprime_product line 71
8. lemma OAI.OrdinarySmoothRough.smooth_coprime_rough line 76
9. lemma OAI.OrdinarySmoothRough.factorization_unique line 83
10. lemma OAI.OrdinarySmoothRough.parts_pos line 93
11. lemma OAI.OrdinarySmoothRough.multiplicative_factorization line 100