OAI/NumberTheory/DirichletL/Detector/PhysicalCRT.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.ProbePhysical.coprime_function_fourier line 13
2. theorem OAI.SevenEighths.ProbePhysical.sexticGauss_coprime_product line 69
3. lemma OAI.SevenEighths.ProbePhysical.elementFourier_const_mul line 97
4. lemma OAI.SevenEighths.ProbePhysical.bareMoving_product line 101
5. theorem OAI.SevenEighths.ProbePhysical.barePhysicalFourier_product line 112
6. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_product line 175
7. lemma OAI.SevenEighths.ProbePhysical.idealRowHom_ne_zero_of_coprime line 199
8. theorem OAI.SevenEighths.ProbePhysical.bareCongruenceCoefficient_product_reduced line 206