OAI/NumberTheory/PiExponent/Polynomials/GradedSerre.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PiExponent.GradedSerre.span_homogeneous_eq line 16
  2. theorem OAI.PiExponent.GradedSerre.exists_finite_homogeneous_generators line 27
  3. theorem OAI.PiExponent.GradedSerre.exists_homogeneous_free_cover line 45
  4. theorem OAI.PiExponent.GradedSerre.kernel_homogeneous line 65
  5. theorem OAI.PiExponent.GradedSerre.exists_finite_homogeneous_relations line 78
  6. theorem OAI.PiExponent.GradedSerre.decompose_smul_homogeneous line 100
  7. theorem OAI.PiExponent.GradedSerre.free_cover_degree_compatible line 120
  8. theorem OAI.PiExponent.GradedSerre.exists_graded_free_map line 134
  9. instance OAI.PiExponent.GradedSerre.shiftedFreeGradedSMul line 159
  10. theorem OAI.PiExponent.GradedSerre.exists_graded_free_presentation line 170
  11. theorem OAI.PiExponent.GradedSerre.eventually_free_twist_cech_exact line 194
  12. theorem OAI.PiExponent.GradedSerre.compatible_vertices_are_polynomial line 218