OAI/NumberTheory/PiExponent/LocalAlgebra/ConePrimeLocalization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSiegel.W17.ConeLocalLength.awayChartPrime line 16
  2. instance OAI.PiExponentSiegel.W17.ConeLocalLength.awayChartPrime_isPrime line 19
  3. def OAI.PiExponentSiegel.W17.ConeLocalLength.conePrime line 23
  4. instance OAI.PiExponentSiegel.W17.ConeLocalLength.conePrime_isPrime line 26
  5. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.homogenizing_coordinate_not_mem_conePrime line 30
  6. def OAI.PiExponentSiegel.W17.ConeLocalLength.conePrimeLocalizationEquiv line 40
  7. def OAI.PiExponentSiegel.W17.ConeLocalLength.affineLocalToConeLocal line 49
  8. def OAI.PiExponentSiegel.W17.ConeLocalLength.affineLocalConeAlgebra line 55
  9. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.affineLocalToConeLocal_map_maximalIdeal line 59
  10. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.affineLocalToConeLocal_flat line 69
  11. theorem OAI.PiExponentSiegel.W17.ConeLocalLength.coneLocal_quotient_length line 83