OAI/NumberTheory/SiegelZeros/LocalAlgebra/ConeRegularSequence.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.W17.ConeLocalLength.conePrimeLocalizationEquiv_algebraMap line 20
  2. theorem OAI.SiegelZeros.W17.ConeLocalLength.conePrimeLocalizationEquiv_map_ideal line 43
  3. theorem OAI.SiegelZeros.W17.ConeLocalLength.affine_ideal_map_to_laurent_local line 55
  4. theorem OAI.SiegelZeros.W17.ConeLocalLength.homogenized_cone_local_length_eq line 69
  5. theorem OAI.SiegelZeros.W17.ConeLocalLength.ofList_map_mul_units line 114
  6. theorem OAI.SiegelZeros.W17.ConeLocalLength.isRegular_map_mul_units line 127
  7. def OAI.SiegelZeros.W17.ConeLocalLength.coneLocalCoordinate line 153
  8. theorem OAI.SiegelZeros.W17.ConeLocalLength.coneLocalCoordinate_isUnit line 156
  9. theorem OAI.SiegelZeros.W17.ConeLocalLength.homogenized_local_eq_affine_mul_coordinate line 161
  10. theorem OAI.SiegelZeros.W17.ConeLocalLength.affineLocalToConeLocal_faithfullyFlat line 192
  11. theorem OAI.SiegelZeros.W17.ConeLocalLength.homogenized_list_regular_at_cone line 205