OAI/NumberTheory/DirichletL/Reflection/ActiveDictionary.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.SevenEighths.InverseReflectedPhase.disjSumIndexEquivline 11 - lemma
OAI.SevenEighths.InverseReflectedPhase.complete_marked_setline 22 - def
OAI.SevenEighths.InverseReflectedPhase.markedActiveEquivline 27 - lemma
OAI.SevenEighths.InverseReflectedPhase.markedActiveEquiv_frozenline 35 - lemma
OAI.SevenEighths.InverseReflectedPhase.markedActiveEquiv_residualline 37 - lemma
OAI.SevenEighths.InverseReflectedPhase.markedActiveEquiv_slotline 39