OAI/NumberTheory/PiExponent/Cohomology/ProjectiveLaurentVertex.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.ChartExponent line 18
  2. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.VertexMonomialSet line 20
  3. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.encode line 23
  4. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.encode_self line 36
  5. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.encode_other line 41
  6. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.encode_regular line 46
  7. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.decode line 51
  8. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.decode_apply line 54
  9. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.decode_encode line 57
  10. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.encode_decode line 62
  11. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.exponentEquiv line 82
  12. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.vertexPolynomialEquiv line 90
  13. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.vertexLaurent line 97
  14. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.vertexLaurent_monomial line 102
  15. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.vertexLaurent_coefficient line 107
  16. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.mem_supported_iff_regular line 114
  17. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.vertexLaurent_regular line 127
  18. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.vertexLaurent_injective line 131
  19. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.vertexLaurent_surjective_regular line 135
  20. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.fullEncode line 152
  21. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.fullEncode_self line 165
  22. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.fullEncode_other line 170
  23. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.fullExponentEquiv line 175
  24. abbrev OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.chartGroupAlgebra line 191
  25. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.natExponentHom line 193
  26. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.polynomialToGroupAlgebra line 198
  27. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.polynomialToGroupAlgebra_injective line 203
  28. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.groupAlgebraToLaurent line 210
  29. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.chartProduct line 213
  30. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.groupAlgebra_single_isUnit line 217
  31. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.polynomialToGroupAlgebra_X line 226
  32. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.groupAlgebra_product_isUnit line 233
  33. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapToGroupAlgebra line 240
  34. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapToGroupAlgebra_base line 246
  35. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapToGroupAlgebra_injective line 252
  36. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapLaurent line 263
  37. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapLaurent_injective line 267
  38. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.productExponent line 271
  39. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.polynomialToGroupAlgebra_product line 275
  40. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.productExponent_outside line 290
  41. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.polynomialToGroupAlgebra_nonnegative line 300
  42. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapToGroupAlgebra_nonnegative line 308
  43. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.groupAlgebraToLaurent_coefficient line 324
  44. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapLaurent_regular line 330
  45. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.fullEncode_nat line 346
  46. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.groupAlgebraToLaurent_polynomial line 349
  47. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapLaurent_base line 363
  48. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapLaurent_natural line 373
  49. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.productExponent_inside line 397
  50. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.exists_cleared_exponent line 402
  51. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.groupAlgebra_single_in_overlap_range line 423
  52. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.laurent_single_in_overlap_range line 444
  53. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentVertex.overlapLaurent_surjective_regular line 457