OAI/NumberTheory/Ostmann/Construction/DiagonalRegroupingMatching.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.remainingValues line 12
2. theorem OAI.Ostmann.Construction.remainingValues_prod line 16
3. theorem OAI.Ostmann.Construction.remainingValues_prime line 20
4. theorem OAI.Ostmann.Construction.reduced_signed_fraction_unique line 29
5. theorem OAI.Ostmann.Construction.remainingProduct_coprime_frequency line 44
6. theorem OAI.Ostmann.Construction.remainingExactTag_eq_iff line 53
7. theorem OAI.Ostmann.Construction.remainingValues_perm_of_product_eq line 68
8. theorem OAI.Ostmann.Construction.remainingValues_nodup_of_integrand_ne_zero line 76
9. theorem OAI.Ostmann.Construction.existsUnique_value_matching line 94