OAI/NumberTheory/DirichletL/Detector/IdealMultiplicative.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.highSupport line 15
2. lemma OAI.SevenEighths.ProbePhysical.highSupport_mul line 18
3. lemma OAI.SevenEighths.ProbePhysical.span_primaryGenerator_of_supported line 25
4. lemma OAI.SevenEighths.ProbePhysical.primaryGenerator_coprime line 29
5. lemma OAI.SevenEighths.ProbePhysical.completed_block_dvd_cube line 34
6. lemma OAI.SevenEighths.ProbePhysical.first_block_dvd line 38
7. lemma OAI.SevenEighths.ProbePhysical.last_block_dvd line 42
8. theorem OAI.SevenEighths.ProbePhysical.bareIdealHighCoefficient_mul line 46
9. lemma OAI.SevenEighths.ProbePhysical.fullIdealWeight_mul line 102
10. theorem OAI.SevenEighths.ProbePhysical.bareIdealHighSummand_mul line 106