OAI/NumberTheory/PiExponent/Cohomology/GradedPolynomialLaurent.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.GradedPolynomialLaurent.GroupAlgebra line 13
  2. def OAI.PiExponent.GradedPolynomialLaurent.natExponentHom line 15
  3. def OAI.PiExponent.GradedPolynomialLaurent.polynomialToGroupAlgebra line 20
  4. theorem OAI.PiExponent.GradedPolynomialLaurent.polynomialToGroupAlgebra_injective line 23
  5. def OAI.PiExponent.GradedPolynomialLaurent.product line 30
  6. def OAI.PiExponent.GradedPolynomialLaurent.productExponent line 32
  7. theorem OAI.PiExponent.GradedPolynomialLaurent.single_isUnit line 34
  8. theorem OAI.PiExponent.GradedPolynomialLaurent.polynomialToGroupAlgebra_X line 42
  9. theorem OAI.PiExponent.GradedPolynomialLaurent.polynomialToGroupAlgebra_product line 48
  10. theorem OAI.PiExponent.GradedPolynomialLaurent.product_isUnit line 61
  11. def OAI.PiExponent.GradedPolynomialLaurent.ringLocalizationMap line 66
  12. theorem OAI.PiExponent.GradedPolynomialLaurent.ringLocalizationMap_base line 70
  13. theorem OAI.PiExponent.GradedPolynomialLaurent.ringLocalizationMap_injective line 74
  14. def OAI.PiExponent.GradedPolynomialLaurent.moduleRingEquiv line 85
  15. theorem OAI.PiExponent.GradedPolynomialLaurent.moduleRingEquiv_fraction line 90
  16. def OAI.PiExponent.GradedPolynomialLaurent.moduleToGroupAlgebra line 96
  17. theorem OAI.PiExponent.GradedPolynomialLaurent.moduleToGroupAlgebra_injective line 101
  18. theorem OAI.PiExponent.GradedPolynomialLaurent.moduleToGroupAlgebra_fraction line 105
  19. theorem OAI.PiExponent.GradedPolynomialLaurent.productExponent_apply line 122
  20. theorem OAI.PiExponent.GradedPolynomialLaurent.sum_productExponent line 129
  21. theorem OAI.PiExponent.GradedPolynomialLaurent.natExponentHom_injective line 134
  22. theorem OAI.PiExponent.GradedPolynomialLaurent.polynomialToGroupAlgebra_coefficient line 140
  23. theorem OAI.PiExponent.GradedPolynomialLaurent.polynomialToGroupAlgebra_support line 144
  24. theorem OAI.PiExponent.GradedPolynomialLaurent.moduleToGroupAlgebra_fraction_coefficient line 157
  25. abbrev OAI.PiExponent.GradedPolynomialLaurent.grading line 164
  26. theorem OAI.PiExponent.GradedPolynomialLaurent.variable_mem line 168
  27. theorem OAI.PiExponent.GradedPolynomialLaurent.product_mem line 172
  28. abbrev OAI.PiExponent.GradedPolynomialLaurent.Piece line 176
  29. theorem OAI.PiExponent.GradedPolynomialLaurent.piece_support line 179
  30. def OAI.PiExponent.GradedPolynomialLaurent.pieceToLaurent line 193
  31. theorem OAI.PiExponent.GradedPolynomialLaurent.pieceToLaurent_coefficient line 199
  32. theorem OAI.PiExponent.GradedPolynomialLaurent.pieceToLaurent_regular line 203
  33. theorem OAI.PiExponent.GradedPolynomialLaurent.pieceToLaurent_injective line 209
  34. theorem OAI.PiExponent.GradedPolynomialLaurent.exists_cleared_exponent line 225
  35. theorem OAI.PiExponent.GradedPolynomialLaurent.single_in_piece_range line 246
  36. theorem OAI.PiExponent.GradedPolynomialLaurent.pieceToLaurent_surjective_regular line 272
  37. theorem OAI.PiExponent.GradedPolynomialLaurent.moduleToGroupAlgebra_smul line 294
  38. theorem OAI.PiExponent.GradedPolynomialLaurent.moduleToGroupAlgebra_restriction line 302
  39. theorem OAI.PiExponent.GradedPolynomialLaurent.pieceToLaurent_restriction line 319