OAI/NumberTheory/PiExponent/Cohomology/GradedH0.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.GradedH0.PolynomialExponent line 12
  2. def OAI.PiExponent.GradedH0.NonnegativeMonomialSet line 14
  3. def OAI.PiExponent.GradedH0.encode line 17
  4. theorem OAI.PiExponent.GradedH0.encode_apply line 21
  5. theorem OAI.PiExponent.GradedH0.encode_nonnegative line 24
  6. def OAI.PiExponent.GradedH0.decode line 27
  7. theorem OAI.PiExponent.GradedH0.decode_apply line 42
  8. def OAI.PiExponent.GradedH0.exponentEquiv line 45
  9. def OAI.PiExponent.GradedH0.homogeneousPolynomialEquiv line 60
  10. theorem OAI.PiExponent.GradedH0.integer_grading_eq_homogeneous line 68
  11. def OAI.PiExponent.GradedH0.integerHomogeneousPolynomialEquiv line 79
  12. def OAI.PiExponent.GradedH0.polynomialLaurent line 88
  13. theorem OAI.PiExponent.GradedH0.mem_supported_iff_regular line 93
  14. theorem OAI.PiExponent.GradedH0.polynomialLaurent_injective line 104
  15. theorem OAI.PiExponent.GradedH0.polynomialLaurent_regular line 108
  16. theorem OAI.PiExponent.GradedH0.existsUnique_polynomial_of_regular line 113
  17. theorem OAI.PiExponent.GradedH0.existsUnique_polynomial_of_compatible_vertices line 127
  18. theorem OAI.PiExponent.GradedH0.zeroth_cocycle_vertices_eq line 139
  19. theorem OAI.PiExponent.GradedH0.zeroth_cocycle_unique_homogeneous_polynomial line 158