OAI/NumberTheory/Jacobsthal/Siegel/PolynomialBox.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.polynomialBox line 17
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.totalDegree_lt_of_mem_polynomialBox line 22
  3. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJetIdeal line 41
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJetIdeal_map line 45
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_prime_height_eq_cotangent_finrank line 50
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangleJetIdeal_exists_parameters_with_length line 62
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.torus_rectangleJetIdeal_exists_bounded_parameters line 124
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.adjoin_fractionField_coordinates line 147
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.adjoin_quotient_coordinates line 164
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_coordinate_transcendence_basis line 175
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_prime_quotient_coordinate_basis line 187
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficient_nonZeroDivisors_disjoint line 204
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficient_localization_prime_height line 217
  14. def OAI.Erdos970.WeightedTorusJets.Geometry.coefficientLocalizationLocalEquiv line 230
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.kernel_isMaximal_of_algebraic_field line 249
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coefficient_localization_isMaximal line 257
  17. def OAI.Erdos970.WeightedTorusJets.Geometry.coordinateFractionAlgebra line 268
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateFractionAlgebra_algebraMap line 275
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.transcendenceBasis_isAlgebraic_coordinateFraction line 285
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateFraction_aeval_comp_map line 297
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateFraction_kernel_isMaximal line 317
  22. def OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit line 340
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_C line 346
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_X_mem line 351
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_X_compl line 356
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_symm_C line 361
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_symm_X_compl line 373
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.aeval_coordinateSplit_symm line 379
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_comap_coefficients_eq_bot line 393
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_comap_coefficients_eq_bot_of_fractionField line 410
  31. def OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplitLocalEquiv line 421
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.totalDegree_coordinateSplit_le line 428
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.totalDegree_localized_coordinateSplit_le line 463
  34. def OAI.Erdos970.WeightedTorusJets.Geometry.componentCoordinate line 472
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.aeval_componentCoordinate line 478
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.ker_aeval_componentCoordinate line 486
  37. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_prime_eq_evaluation_kernel line 496
  38. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coordinateSplit_localized_prime_isMaximal line 511