OAI/NumberTheory/PowerFree/ProjectionDegrees.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.polynomial_projection_hilbert_le line 11
  2. theorem OAI.QuarticPowerFree.polynomial_projection_equation_degree_bound line 36
  3. theorem OAI.QuarticPowerFree.polynomial_projection_equation_degree_bound_equiv line 77
  4. theorem OAI.QuarticPowerFree.affine_polynomial_projection_degree_bound line 107
  5. theorem OAI.QuarticPowerFree.left_coordinates_transcendence_selection line 121
  6. theorem OAI.QuarticPowerFree.pair_right_isAlgebraic line 166
  7. theorem OAI.QuarticPowerFree.pair_projection_isAlgebraic line 190
  8. theorem OAI.QuarticPowerFree.principal_evaluation_kernel_reindex line 209
  9. def OAI.QuarticPowerFree.pairProjectionIndex line 230
  10. theorem OAI.QuarticPowerFree.pairProjectionIndex_zero line 233
  11. theorem OAI.QuarticPowerFree.pairProjectionIndex_one line 236
  12. theorem OAI.QuarticPowerFree.pairProjectionIndex_succ_succ line 239
  13. theorem OAI.QuarticPowerFree.finite_basis_extra_dependent line 249
  14. theorem OAI.QuarticPowerFree.pairProjectionIndex_evaluation line 259
  15. theorem OAI.QuarticPowerFree.pair_principal_projection_of_extra line 270
  16. theorem OAI.QuarticPowerFree.pair_principal_projection_of_basis line 287
  17. theorem OAI.QuarticPowerFree.pair_principal_projection_selection line 320