OAI/NumberTheory/DirichletL/Reflection/Moving.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseReflectedPhase.reflectedExponent line 11
2. def OAI.SevenEighths.InverseReflectedPhase.frozenIndices line 14
3. def OAI.SevenEighths.InverseReflectedPhase.residualIndices line 17
4. def OAI.SevenEighths.InverseReflectedPhase.slotIndices line 20
5. lemma OAI.SevenEighths.InverseReflectedPhase.reflected_indices_partition line 23
6. lemma OAI.SevenEighths.InverseReflectedPhase.reflected_residual_exponent line 42
7. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.reflected_residual_product line 50
8. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.reflected_slot_product line 60
9. theorem OAI.SevenEighths.InverseReflectedPhase.moving_common_reflected_coefficients line 71