OAI/NumberTheory/PowerFree/UnitBalancing.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.lattice_covering_radius line 13
  2. theorem OAI.QuarticPowerFree.logarithmic_units_cover line 30
  3. theorem OAI.QuarticPowerFree.unit_balancing_hyperplane line 39
  4. theorem OAI.QuarticPowerFree.unit_balancing_norm line 87
  5. theorem OAI.QuarticPowerFree.finite_ideal_correction line 137
  6. theorem OAI.QuarticPowerFree.balanced_ideal_factorization line 175
  7. theorem OAI.QuarticPowerFree.arithmetic_factorization_large_primes line 214
  8. structure OAI.QuarticPowerFree.ArithmeticModel line 285
  9. def OAI.QuarticPowerFree.arithmeticModel line 299
  10. theorem OAI.QuarticPowerFree.uniform_root_difference_bounds line 338
  11. theorem OAI.QuarticPowerFree.absorb_finite_ideal_norms line 363
  12. theorem OAI.QuarticPowerFree.companion_archimedean_bounds line 401
  13. theorem OAI.QuarticPowerFree.balanced_arithmetic line 436