OAI/NumberTheory/DirichletL/Detector/LowRay.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.ProbePhysical.PhysicalRayElement line 13
2. def OAI.SevenEighths.ProbePhysical.physicalRay line 15
3. def OAI.SevenEighths.ProbePhysical.physicalRayRepresentative line 17
4. lemma OAI.SevenEighths.ProbePhysical.physicalRayRepresentative_spec line 24
5. lemma OAI.SevenEighths.ProbePhysical.rowCoefficient_congr_ray line 30
6. def OAI.SevenEighths.ProbePhysical.physicalRayRowMonoid line 42
7. def OAI.SevenEighths.ProbePhysical.physicalIdealRay line 46
8. lemma OAI.SevenEighths.ProbePhysical.physicalRowMonoid_eq_ray line 48
9. lemma OAI.SevenEighths.ProbePhysical.physicalRayRowMonoid_norm line 55
10. def OAI.SevenEighths.ProbePhysical.physicalRayPeriodicBase line 59
11. theorem OAI.SevenEighths.ProbePhysical.physicalRayPeriodicBase_uniform line 65
12. theorem OAI.SevenEighths.ProbePhysical.physicalRayRow_eq_periodic_inverse line 75