OAI/NumberTheory/DirichletL/Detector/LowPrimeFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalSelectedPrime_maximal line 14
2. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalSelectedPrime_good line 21
3. def OAI.SevenEighths.ProbePhysical.lowCanonicalPrimeFamily line 30
4. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalPrimeFamily_generator line 38
5. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalPrimeFamily_pairwise line 48
6. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalPrimeFamily_odd line 55
7. lemma OAI.SevenEighths.ProbePhysical.lowCanonicalPrimeFamily_product line 61
8. theorem OAI.SevenEighths.ProbePhysical.lowCanonicalInverseRow_eq line 70