OAI/NumberTheory/SiegelZeros/LocalAlgebra/RectangularLocalization.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.W23.jetConstant line 15
  2. theorem OAI.SiegelZeros.W23.jet_coordinate_nilpotent line 18
  3. theorem OAI.SiegelZeros.W23.jet_nilpotent_sub_constant line 25
  4. theorem OAI.SiegelZeros.W23.jet_nilpotent_transfer line 36
  5. def OAI.SiegelZeros.W23.rectangleConstant line 46
  6. theorem OAI.SiegelZeros.W23.rectangle_nilpotent_sub_constant line 50
  7. theorem OAI.SiegelZeros.W23.rectangularJetHom_nilpotent_correction line 67
  8. theorem OAI.SiegelZeros.W23.rectangularJetHom_isUnit line 77
  9. def OAI.SiegelZeros.W23.localizedRectangularJet line 85
  10. theorem OAI.SiegelZeros.W23.localizedRectangularJet_algebraMap line 91
  11. theorem OAI.SiegelZeros.W23.localized_generator_span_le_ker line 100
  12. def OAI.SiegelZeros.W23.localizedGeneratorQuotient line 114