OAI/NumberTheory/SiegelZeros/Structure/CodimensionOne.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W58.torus_integrallyClosed line 17
2. theorem OAI.SiegelZeros.W58.generic_local_isDomain line 22
3. theorem OAI.SiegelZeros.W58.generic_local_integrallyClosed line 30
4. theorem OAI.SiegelZeros.W58.dvr_of_local_normal_dimension_one line 37
5. theorem OAI.SiegelZeros.W58.generic_local_dvr_of_height_one line 54
6. theorem OAI.SiegelZeros.W58.generic_cotangent_finrank_of_height_one line 61
7. theorem OAI.SiegelZeros.W58.generic_local_regular_of_height_one line 70