OAI/NumberTheory/DukePrimeDegree/Arithmetic/ConductorModulus.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An integer modulus for finitely many local congruences

The product of norms of conductor primes, raised to their conductor exponents, gives a rational integer imposing every required local higher-unit congruence. No quantitative conductor bound is needed.

  1. theorem OAI.DukePrimeDegree.integral_mem_completed_maximal line 22
  2. theorem OAI.DukePrimeDegree.exists_integer_for_local_congruences line 32
  3. theorem OAI.DukePrimeDegree.completed_congruence_of_integer line 56
  4. theorem OAI.DukePrimeDegree.completed_integral_isUnit_of_congruence line 68