OAI/NumberTheory/SiegelZeros/LocalAlgebra/CoordinateQuotientGrading.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.W64.quotientSection line 17
  2. instance OAI.SiegelZeros.WeightedTorusJets.W64.quotientSection_finite line 21
  3. def OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionMultiply line 26
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionMultiply_injective line 40
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W64.quotientSectionCokernel_finrank_add line 48
  6. def OAI.SiegelZeros.W08.coordinateEval line 76
  7. def OAI.SiegelZeros.W08.coordinateInclude line 79
  8. theorem OAI.SiegelZeros.W08.coordinateEval_X_none line 82
  9. theorem OAI.SiegelZeros.W08.coordinateEval_X_some line 85
  10. theorem OAI.SiegelZeros.W08.coordinateEval_include line 88
  11. theorem OAI.SiegelZeros.W08.coordinateEval_surjective line 95
  12. theorem OAI.SiegelZeros.W08.coordinateEval_homogeneous line 99
  13. theorem OAI.SiegelZeros.W08.coordinateInclude_homogeneous line 108
  14. def OAI.SiegelZeros.W08.coordinateImageIdeal line 112
  15. theorem OAI.SiegelZeros.W08.homogeneous_ideal_map_of_degree_preserving line 115
  16. theorem OAI.SiegelZeros.W08.coordinateImageIdeal_homogeneous line 128
  17. theorem OAI.SiegelZeros.W08.coordinateInclude_eval_mod line 134
  18. def OAI.SiegelZeros.W08.coordinateQuotientMap line 145
  19. theorem OAI.SiegelZeros.W08.coordinateInclude_image_mem line 150
  20. def OAI.SiegelZeros.W08.coordinateQuotientInverse line 160
  21. def OAI.SiegelZeros.W08.coordinateQuotientEquiv line 166
  22. theorem OAI.SiegelZeros.W08.coordinateQuotientEquiv_mk line 182
  23. theorem OAI.SiegelZeros.W08.coordinateQuotientEquiv_section_map line 192
  24. def OAI.SiegelZeros.W08.coordinateQuotientSectionEquiv line 211
  25. theorem OAI.SiegelZeros.W08.coordinateQuotientSection_finrank line 219
  26. def OAI.SiegelZeros.W08.renameQuotientEquiv line 233
  27. theorem OAI.SiegelZeros.W08.renameQuotientEquiv_section_map line 239
  28. def OAI.SiegelZeros.W08.renameQuotientSectionEquiv line 257
  29. theorem OAI.SiegelZeros.W08.renameQuotientSection_finrank line 265
  30. theorem OAI.SiegelZeros.W08.renameImageIdeal_homogeneous line 273