OAI/NumberTheory/Ostmann/Construction/GiantCoprimeRemoval.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Removing only the top-giant coprimality test under the original laws

  1. theorem OAI.Ostmann.weighted_coprime_removal_bound line 11
  2. theorem OAI.Ostmann.weighted_prime_coprime_removal line 34
  3. theorem OAI.Ostmann.integer_bad_coprime_mass line 63
  4. theorem OAI.Ostmann.weighted_integer_prime_coprime_removal line 87