OAI/NumberTheory/DirichletL/Detector/LowPeriod.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.calibrationRowModulus line 15
2. def OAI.SevenEighths.ProbePhysical.periodicCalibrationXi line 18
3. lemma OAI.SevenEighths.ProbePhysical.calibrationRowModulus_ne_zero line 22
4. lemma OAI.SevenEighths.ProbePhysical.periodicCalibrationXi_norm line 32
5. lemma OAI.SevenEighths.ProbePhysical.periodicCalibrationXi_periodic line 38
6. lemma OAI.SevenEighths.ProbePhysical.periodicCalibrationXi_eq_primary line 50
7. def OAI.SevenEighths.ProbePhysical.lowPeriodicBase line 65
8. def OAI.SevenEighths.ProbePhysical.lowBaseModulus line 70
9. lemma OAI.SevenEighths.ProbePhysical.lowBaseModulus_ne_zero line 74
10. lemma OAI.SevenEighths.ProbePhysical.lowPeriodicBase_periodic line 83
11. lemma OAI.SevenEighths.ProbePhysical.lowPeriodicBase_norm line 99
12. lemma OAI.SevenEighths.ProbePhysical.lowPeriodicBase_eq_primary line 107