OAI/NumberTheory/PowerFree/NormComponents.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.quotient_pair_generates line 11
  2. theorem OAI.QuarticPowerFree.norm_dimension_le line 27
  3. theorem OAI.QuarticPowerFree.polynomial_constant_at_point line 44
  4. theorem OAI.QuarticPowerFree.algebraic_polynomial_fibre_count line 53
  5. theorem OAI.QuarticPowerFree.algebraic_left_fibre_count line 64
  6. theorem OAI.QuarticPowerFree.norm_generic_threshold_uniform line 87
  7. theorem OAI.QuarticPowerFree.norm_full_threshold_uniform line 119
  8. structure OAI.QuarticPowerFree.NormBoxSystem line 154
  9. def OAI.QuarticPowerFree.NormBoxSystem.a line 176
  10. def OAI.QuarticPowerFree.NormBoxSystem.equation line 180
  11. def OAI.QuarticPowerFree.NormBoxSystem.ideal line 184
  12. theorem OAI.QuarticPowerFree.NormBoxSystem.quotient_equations line 188
  13. theorem OAI.QuarticPowerFree.NormBoxSystem.quotient_left_nonzero line 200
  14. theorem OAI.QuarticPowerFree.NormBoxSystem.right_real_weight line 211
  15. theorem OAI.QuarticPowerFree.norm_component_alternatives line 223