OAI/NumberTheory/DukePrimeDegree/Arithmetic/ClassFieldModulus.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A common even modulus away from ramification

Enlarging the finite conductor to contain the discriminant primes leaves its infinite part empty and its Artin-kernel property intact. An ordinary positive integer then imposes all of its local congruences.

  1. theorem OAI.DukePrimeDegree.exists_even_unramified_artin_modulus line 25
  2. theorem OAI.DukePrimeDegree.exists_integer_even_artin_modulus line 59