OAI/NumberTheory/SiegelZeros/Intersection/NormalIntersection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.baseFractions line 22
  2. def OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.denominatorIdeal line 24
  3. lemma OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.mem_denominatorIdeal line 27
  4. lemma OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.denominatorIdeal_ne_bot line 32
  5. lemma OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.fraction_in_base_of_preserves_ideal line 42
  6. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.prime_denominatorIdeal_height_eq_one line 58
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.Workers.W15.mem_base_of_mem_heightOne_localizations line 97