OAI/NumberTheory/DirichletL/Reflection/Pullback.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.InverseReflectedPhase.pullback_generator_eqline 15 - def
OAI.SevenEighths.InverseReflectedPhase.pullbackControlledline 20 - lemma
OAI.SevenEighths.InverseReflectedPhase.reindexMarks_symmline 25 - theorem
OAI.SevenEighths.InverseReflectedPhase.mixedReflectedValue_pullbackline 30