OAI/NumberTheory/DirichletL/UnitSexticWitness.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.UnitSexticWitness.idealRowHom_unit_eq_of_norm_mod_seven line 15
2. lemma OAI.SevenEighths.UnitSexticWitness.prime_norm_good line 29
3. lemma OAI.SevenEighths.UnitSexticWitness.prime_norm_ringChar line 39
4. lemma OAI.SevenEighths.UnitSexticWitness.exists_primeIdeal_norm line 50
5. theorem OAI.SevenEighths.UnitSexticWitness.exists_prime_unit_embedding line 65
6. theorem OAI.SevenEighths.UnitSexticWitness.exists_unit_witness line 90
7. theorem OAI.SevenEighths.UnitSexticWitness.exists_prime_embedding_after_deletion line 106
8. theorem OAI.SevenEighths.UnitSexticWitness.deleted_unit_row_ne_principal line 122