OAI/NumberTheory/PiExponent/Polynomials/CoordinateQuotientGrading.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSiegel.W08.coordinateEval line 17
  2. def OAI.PiExponentSiegel.W08.coordinateInclude line 20
  3. theorem OAI.PiExponentSiegel.W08.coordinateEval_X_none line 23
  4. theorem OAI.PiExponentSiegel.W08.coordinateEval_X_some line 26
  5. theorem OAI.PiExponentSiegel.W08.coordinateEval_include line 29
  6. theorem OAI.PiExponentSiegel.W08.coordinateEval_surjective line 36
  7. theorem OAI.PiExponentSiegel.W08.coordinateEval_homogeneous line 40
  8. theorem OAI.PiExponentSiegel.W08.coordinateInclude_homogeneous line 49
  9. def OAI.PiExponentSiegel.W08.coordinateImageIdeal line 53
  10. theorem OAI.PiExponentSiegel.W08.homogeneous_ideal_map_of_degree_preserving line 56
  11. theorem OAI.PiExponentSiegel.W08.coordinateImageIdeal_homogeneous line 69
  12. theorem OAI.PiExponentSiegel.W08.coordinateInclude_eval_mod line 75
  13. def OAI.PiExponentSiegel.W08.coordinateQuotientMap line 86
  14. theorem OAI.PiExponentSiegel.W08.coordinateInclude_image_mem line 91
  15. def OAI.PiExponentSiegel.W08.coordinateQuotientInverse line 101
  16. def OAI.PiExponentSiegel.W08.coordinateQuotientEquiv line 107
  17. theorem OAI.PiExponentSiegel.W08.coordinateQuotientEquiv_mk line 123
  18. theorem OAI.PiExponentSiegel.W08.coordinateQuotientEquiv_section_map line 128
  19. def OAI.PiExponentSiegel.W08.coordinateQuotientSectionEquiv line 147
  20. theorem OAI.PiExponentSiegel.W08.coordinateQuotientSection_finrank line 154
  21. def OAI.PiExponentSiegel.W08.renameQuotientEquiv line 164
  22. theorem OAI.PiExponentSiegel.W08.renameQuotientEquiv_section_map line 169
  23. def OAI.PiExponentSiegel.W08.renameQuotientSectionEquiv line 187
  24. theorem OAI.PiExponentSiegel.W08.renameQuotientSection_finrank line 194
  25. theorem OAI.PiExponentSiegel.W08.renameImageIdeal_homogeneous line 201