OAI/NumberTheory/PowerFree/PointInterpolation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuarticPowerFree.exists_mv_interpolate line 16
  2. theorem OAI.QuarticPowerFree.card_points_le_hilbert_constant line 48
  3. theorem OAI.QuarticPowerFree.affineDimension_independent_coordinates line 110
  4. theorem OAI.QuarticPowerFree.determined_bounded_patch line 123
  5. theorem OAI.QuarticPowerFree.point_on_minimal_component line 150
  6. theorem OAI.QuarticPowerFree.proper_cut_components line 159
  7. theorem OAI.QuarticPowerFree.zeroDim_isMaximal line 192
  8. theorem OAI.QuarticPowerFree.zeroDim_eq_point line 202
  9. theorem OAI.QuarticPowerFree.zeroDim_determined line 209
  10. structure OAI.QuarticPowerFree.IntegerPatch line 225
  11. def OAI.QuarticPowerFree.IntegerPatch.minor line 229
  12. def OAI.QuarticPowerFree.IntegerPatch.On line 232
  13. def OAI.QuarticPowerFree.IntegerPatch.Bounded line 238
  14. def OAI.QuarticPowerFree.PointOn line 243
  15. theorem OAI.QuarticPowerFree.IntegerPatch.Bounded.mono line 247
  16. theorem OAI.QuarticPowerFree.map_integer_minor line 252
  17. theorem OAI.QuarticPowerFree.determined_integer_patch line 264
  18. theorem OAI.QuarticPowerFree.IntegerPatch.minor_degree_le line 278
  19. theorem OAI.QuarticPowerFree.bounded_cut_components line 286