OAI/NumberTheory/DukePrimeDegree/Arithmetic/ClassFieldCongruences.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Rational congruences give principal ray ideals

Only a finite modulus is needed for a totally real extension. An integer divisible by the selected local prime powers imposes its higher-unit conditions on every nonzero integral element congruent to one.

  1. theorem OAI.DukePrimeDegree.principal_local_mem_higherUnits line 23
  2. theorem OAI.DukePrimeDegree.principalIdele_mem_even_ray_of_congruence line 48