OAI/NumberTheory/DirichletL/Detector/RowRadicalConductor.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.ProbeRowRadicalConductor.canonicalPrimePower_descent line 14
  2. theorem OAI.SevenEighths.ProbeRowRadicalConductor.idealRowHom_congr_radical line 20
  3. theorem OAI.SevenEighths.ProbeRowRadicalConductor.radical_ne_bot line 40
  4. theorem OAI.SevenEighths.ProbeRowRadicalConductor.movingNumeratorRow_radical_periodic line 44
  5. theorem OAI.SevenEighths.ProbeRowRadicalConductor.actualPeriodicRow_radical_periodic line 49
  6. theorem OAI.SevenEighths.ProbeRowRadicalConductor.rowTwist_radical_periodic line 68
  7. theorem OAI.SevenEighths.ProbeRowRadicalConductor.rowTwist_nonzero_radical_unit line 88
  8. theorem OAI.SevenEighths.ProbeRowRadicalConductor.exists_row_character_radical line 101
  9. theorem OAI.SevenEighths.ProbeRowRadicalConductor.periodic_sup line 138
  10. theorem OAI.SevenEighths.ProbeRowRadicalConductor.primitive_of_equal_elements line 148
  11. theorem OAI.SevenEighths.ProbeRowRadicalConductor.rawRow_small_presentation line 198
  12. theorem OAI.SevenEighths.ProbeRowRadicalConductor.rawRow_primitive_radical line 217
  13. theorem OAI.SevenEighths.ProbeRowRadicalConductor.equal_elements_excludePrimes line 228
  14. def OAI.SevenEighths.ProbeRowRadicalConductor.fixedConductorConstant line 242
  15. theorem OAI.SevenEighths.ProbeRowRadicalConductor.rowCharacter_primitive_radical line 245
  16. theorem OAI.SevenEighths.ProbeRowRadicalConductor.prod_le_radical_prod_pow line 264
  17. theorem OAI.SevenEighths.ProbeRowRadicalConductor.radical_norm_selected_deficit line 276
  18. theorem OAI.SevenEighths.ProbeRowRadicalConductor.rowCharacter_primitive_selected_deficit line 318
  19. theorem OAI.SevenEighths.ProbeRowRadicalConductor.canonicalCRT_radical_congr line 341
  20. theorem OAI.SevenEighths.ProbeRowRadicalConductor.fixedConductorConstant_pos line 354
  21. theorem OAI.SevenEighths.ProbeRowRadicalConductor.sourceRow_primitive_radical line 364
  22. theorem OAI.SevenEighths.ProbeRowRadicalConductor.rowCharacter_primitive_selected_div line 380