OAI/NumberTheory/DirichletL/Detector/IdealFactorization.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SevenEighths.ProbePhysical.PrimeIdeal line 13
2. def OAI.SevenEighths.ProbePhysical.primeValuations line 15
3. def OAI.SevenEighths.ProbePhysical.idealFromValuations line 18
4. lemma OAI.SevenEighths.ProbePhysical.idealFromValuations_ne_zero line 21
5. lemma OAI.SevenEighths.ProbePhysical.primeValuations_apply line 25
6. lemma OAI.SevenEighths.ProbePhysical.primeValuations_one line 29
7. lemma OAI.SevenEighths.ProbePhysical.primeValuations_mul line 32
8. lemma OAI.SevenEighths.ProbePhysical.primeValuations_prime line 36
9. lemma OAI.SevenEighths.ProbePhysical.primeValuations_pow line 47
10. lemma OAI.SevenEighths.ProbePhysical.idealFromValuations_zero line 53
11. lemma OAI.SevenEighths.ProbePhysical.idealFromValuations_add line 56
12. lemma OAI.SevenEighths.ProbePhysical.idealFromValuations_single line 60
13. theorem OAI.SevenEighths.ProbePhysical.primeValuations_idealFromValuations line 64
14. theorem OAI.SevenEighths.ProbePhysical.idealFromValuations_primeValuations line 74
15. def OAI.SevenEighths.ProbePhysical.nonzeroIdealValuationEquiv line 85
16. lemma OAI.SevenEighths.ProbePhysical.primeIdeal_coprime line 91
17. lemma OAI.SevenEighths.ProbePhysical.prime_coprime_idealFromValuations line 98
18. def OAI.SevenEighths.ProbePhysical.finsuppPairEquiv line 108
19. abbrev OAI.SevenEighths.ProbePhysical.HighValuation line 119
20. abbrev OAI.SevenEighths.ProbePhysical.NonzeroIdeal line 120
21. def OAI.SevenEighths.ProbePhysical.highValuationEquiv line 122
22. lemma OAI.SevenEighths.ProbePhysical.highValuationEquiv_apply line 129