OAI/NumberTheory/DirichletL/Detector/LowSlotMarks.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbePhysical.lowSelectedIdeal_eq_product line 13
2. lemma OAI.SevenEighths.ProbePhysical.lowSelectedIdeal_dvd_iff line 19
3. lemma OAI.SevenEighths.ProbePhysical.lowSelectedIdeal_mark line 29
4. def OAI.SevenEighths.ProbePhysical.lowCanonicalSelectedPrime line 42
5. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalSelectedPrime_mem line 47
6. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalSelectedPrime_span line 53
7. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalSelectedPrime_injective line 61
8. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalSelected_coprime line 71
9. theorem OAI.SevenEighths.ProbePhysical.lowCanonicalSelected_mark line 79