OAI/NumberTheory/DirichletL/Reflection/CanonicalPool.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily line 11
2. def OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenExponent line 19
3. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenExponent_lt line 22
4. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_pairwise line 26
5. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_odd line 31
6. lemma OAI.SevenEighths.InverseReflectedPhase.maximal_coprime_of_not_dvd line 36
7. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_row_coprime line 41
8. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_level_coprime line 47
9. theorem OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenExponent_on_fiber line 55
10. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_row_coprime_on_fiber line 65
11. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_extracted line 76
12. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_divides_on_fiber line 85
13. lemma OAI.SevenEighths.InverseReflectedPhase.canonicalFrozenFamily_nonresidual_on_fiber line 95