OAI/NumberTheory/DirichletL/Detector/MarkedValuations.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbePhysical.prime_dvd_iff_valuation line 13
2. lemma OAI.SevenEighths.ProbePhysical.prime_dvd_high_completed line 18
3. lemma OAI.SevenEighths.ProbePhysical.primeProduct_dvd line 27
4. def OAI.SevenEighths.ProbePhysical.completedValuationMark line 35
5. lemma OAI.SevenEighths.ProbePhysical.completedValuationMark_norm line 38
6. lemma OAI.SevenEighths.ProbePhysical.completedValuationMark_product line 43
7. lemma OAI.SevenEighths.ProbePhysical.highIdealMask_mark line 59
8. lemma OAI.SevenEighths.ProbePhysical.markedIdealHighSummand_mark line 65