OAI/NumberTheory/PiExponent/Cohomology/ProjectiveLaurentTransitions.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.standardExponent line 13
  2. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.standardExponent_self line 16
  3. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.standardExponent_other line 20
  4. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.zeroDegreeExponent line 23
  5. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.zeroDegreeExponent_injective line 40
  6. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.fullEncode_eq_standard_add line 46
  7. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.zeroDegreeExponent_coordinate line 56
  8. abbrev OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.FullGroupAlgebra line 70
  9. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.chartToFull line 72
  10. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.chartToFull_injective line 75
  11. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.laurentToFull line 78
  12. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.laurentToFull_injective line 82
  13. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.laurentToFull_single line 86
  14. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.laurentToFull_groupAlgebraToLaurent line 90
  15. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapToFull line 104
  16. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapToFull_injective line 108
  17. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.laurentToFull_overlapLaurent line 112
  18. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapToFull_X line 118
  19. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapToFull_C line 124
  20. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapToFull_natural_of_generators line 133
  21. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapLaurent_change_pivot line 151
  22. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapLaurent_change_pivot_pow line 171
  23. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.fullMonomialUnit line 187
  24. def OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.fullMonomialUnits line 193
  25. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.fullMonomialUnit_zpow line 204
  26. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.map_coordinate_unit_zpow line 209
  27. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapLaurent_change_pivot_zpow line 226
  28. theorem OAI.PiExponent.GeometrySupport.ProjectiveLaurentTransitions.overlapToFull_ratio line 243