OAI/NumberTheory/PowerFree/PureCuts.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.prime_height_le_of_goingDown line 16
  2. theorem OAI.QuarticPowerFree.mvPolynomial_maximal_height line 32
  3. theorem OAI.QuarticPowerFree.normalization_size_le_maximal_height line 52
  4. theorem OAI.QuarticPowerFree.normalization_trdeg line 65
  5. theorem OAI.QuarticPowerFree.finite_type_trdeg_le_maximal_height line 81
  6. theorem OAI.QuarticPowerFree.trdeg_le_one_of_principal_maximal line 89
  7. theorem OAI.QuarticPowerFree.localized_algebraic_prime_isMaximal line 102
  8. theorem OAI.QuarticPowerFree.principal_minimal_trdeg_bound_of_normalization line 151
  9. theorem OAI.QuarticPowerFree.principal_minimal_trdeg_bound line 213
  10. theorem OAI.QuarticPowerFree.quotient_hilbert_le line 234
  11. theorem OAI.QuarticPowerFree.cut_minimal_hilbert_codim_le_one line 251
  12. theorem OAI.QuarticPowerFree.proper_cut_hilbert_purity line 279