OAI/NumberTheory/DirichletL/Reflection/Canonical.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SevenEighths.InverseReflectedPhase.PrimeFamily line 12
2. instance OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.idealMaximal line 19
3. def OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator line 21
4. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_ne_zero line 23
5. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_span line 24
6. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_primary line 26
7. instance OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generatorMaximal line 28
8. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_good line 30
9. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_product line 34
10. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_product_primary line 42
11. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_coprime_period line 45
12. lemma OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.generator_product_coprime_period line 52
13. theorem OAI.SevenEighths.InverseReflectedPhase.PrimeFamily.exists_controlled line 59
14. theorem OAI.SevenEighths.InverseReflectedPhase.canonical_common_reflected_coefficients line 77