OAI/NumberTheory/DirichletL/PrimeRows/Valuation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbeHighRowFamily.unitPart line 12
2. theorem OAI.SevenEighths.ProbeHighRowFamily.unitPart_spec line 15
3. theorem OAI.SevenEighths.ProbeHighRowFamily.unitPart_coprime line 19
4. theorem OAI.SevenEighths.ProbeHighRowFamily.unitPart_ne_zero line 22
5. theorem OAI.SevenEighths.ProbeHighRowFamily.multiplicity_lt_six line 28
6. theorem OAI.SevenEighths.ProbeHighRowFamily.canonical_decomposition line 44
7. theorem OAI.SevenEighths.ProbeHighRowFamily.idealRowHighLocalFactor_canonical line 50