OAI/NumberTheory/DirichletL/Detector/LowSlotSplit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.ProbePhysical.LowUnselectedTuple line 10
2. abbrev OAI.SevenEighths.ProbePhysical.LowSelectedTuple line 12
3. def OAI.SevenEighths.ProbePhysical.lowSlotTupleEquiv line 15
4. def OAI.SevenEighths.ProbePhysical.lowSlotJoin line 31
5. lemma OAI.SevenEighths.ProbePhysical.lowSlotJoin_nonzero line 35
6. lemma OAI.SevenEighths.ProbePhysical.lowSlotJoin_unselected line 40
7. lemma OAI.SevenEighths.ProbePhysical.lowSlotJoin_selected line 45
8. lemma OAI.SevenEighths.ProbePhysical.lowSlotJoin_unselectedProduct line 51
9. lemma OAI.SevenEighths.ProbePhysical.lowSlotJoin_selectedProduct line 58
10. lemma OAI.SevenEighths.ProbePhysical.lowSlotJoin_selectedFactor line 65
11. theorem OAI.SevenEighths.ProbePhysical.sum_lowSlotJoin line 74