OAI/NumberTheory/DirichletL/Reflection/Reindex.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.SevenEighths.InverseReflectedPhase.cofactor_reindexline 12 - lemma
OAI.SevenEighths.InverseReflectedPhase.finiteCrossNumerator_reindexline 21 - def
OAI.SevenEighths.InverseReflectedPhase.unitFrequencyEquivline 28 - lemma
OAI.SevenEighths.InverseReflectedPhase.unitFrequencyEquiv_applyline 33 - lemma
OAI.SevenEighths.InverseReflectedPhase.unitFrequencyEquiv_oneline 38 - def
OAI.SevenEighths.InverseReflectedPhase.reindexControlledline 44