OAI/NumberTheory/DirichletL/Reflection/OriginalSlotSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.InverseReflectedPhase.originalSlotChoices line 23
2. def OAI.SevenEighths.InverseReflectedPhase.originalSlotSupportEquiv line 26
3. def OAI.SevenEighths.InverseReflectedPhase.originalSlotSplit line 35
4. lemma OAI.SevenEighths.InverseReflectedPhase.originalSlotSplit_symm_val line 41
5. theorem OAI.SevenEighths.InverseReflectedPhase.original_supported_slot_sum line 47