OAI/NumberTheory/Jacobsthal/Estimates/ActualUnitClasses.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosUnitLifts.radical line 13
  2. theorem OAI.Erdos970.ErdosUnitLifts.radical_pos line 15
  3. theorem OAI.Erdos970.ErdosUnitLifts.radical_dvd line 18
  4. theorem OAI.Erdos970.ErdosUnitLifts.radical_primeFactors line 20
  5. theorem OAI.Erdos970.ErdosUnitLifts.totient_radical line 23
  6. theorem OAI.Erdos970.ErdosUnitLifts.totient_lift_modulus line 29
  7. theorem OAI.Erdos970.ErdosUnitLifts.totient_lift_modulus' line 37
  8. abbrev OAI.Erdos970.ErdosUnitLifts.PrimeIndex line 42
  9. theorem OAI.Erdos970.ErdosUnitLifts.primeIndex_coprime line 44
  10. def OAI.Erdos970.ErdosUnitLifts.localAllowed line 54
  11. theorem OAI.Erdos970.ErdosUnitLifts.affine_eq_iff line 57
  12. theorem OAI.Erdos970.ErdosUnitLifts.localAllowed_card line 69
  13. def OAI.Erdos970.ErdosUnitLifts.crtNat line 77
  14. theorem OAI.Erdos970.ErdosUnitLifts.mem_crtNat line 82
  15. theorem OAI.Erdos970.ErdosUnitLifts.crtNat_card line 103
  16. def OAI.Erdos970.ErdosUnitLifts.allowedK line 111
  17. theorem OAI.Erdos970.ErdosUnitLifts.allowedK_card line 115
  18. def OAI.Erdos970.ErdosUnitLifts.actualN line 157
  19. def OAI.Erdos970.ErdosUnitLifts.actualClasses line 159
  20. def OAI.Erdos970.ErdosUnitLifts.baseResidue line 164
  21. theorem OAI.Erdos970.ErdosUnitLifts.baseResidue_lt line 167
  22. theorem OAI.Erdos970.ErdosUnitLifts.baseResidue_integral line 171
  23. theorem OAI.Erdos970.ErdosUnitLifts.integral_iff_base_mod line 180
  24. theorem OAI.Erdos970.ErdosUnitLifts.base_coprime line 196
  25. theorem OAI.Erdos970.ErdosUnitLifts.actualN_lift line 207
  26. theorem OAI.Erdos970.ErdosUnitLifts.lift_coprime line 214
  27. theorem OAI.Erdos970.ErdosUnitLifts.canonical_lift_iff line 220
  28. theorem OAI.Erdos970.ErdosUnitLifts.actualClasses_eq_lifts line 236
  29. theorem OAI.Erdos970.ErdosUnitLifts.actualClasses_card line 265
  30. theorem OAI.Erdos970.ErdosUnitLifts.actualClasses_reduced line 275
  31. theorem OAI.Erdos970.ErdosUnitLifts.actualClasses_fraction line 286
  32. theorem OAI.Erdos970.ErdosUnitLifts.intCast_isUnit_of_natAbs_coprime line 295
  33. theorem OAI.Erdos970.ErdosUnitLifts.actual_unit_lift_packet line 305
  34. theorem OAI.Erdos970.ErdosUnitLifts.actualClasses_one line 315
  35. theorem OAI.Erdos970.ErdosUnitLifts.actual_lift_forbidden_iff line 318
  36. def OAI.Erdos970.ErdosUnitLifts.reducedClasses line 329
  37. theorem OAI.Erdos970.ErdosUnitLifts.reducedClasses_card line 332
  38. theorem OAI.Erdos970.ErdosUnitLifts.actual_unit_lift_finite_fraction line 335