OAI/NumberTheory/SiegelZeros/LocalAlgebra/PolynomialBox.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialBox line 16
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.totalDegree_lt_of_mem_polynomialBox line 21
  3. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetIdeal line 40
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetIdeal_map line 44
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_prime_height_eq_cotangent_finrank line 49
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetIdeal_exists_parameters_with_length line 61
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.torus_rectangleJetIdeal_exists_bounded_parameters line 123
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.adjoin_fractionField_coordinates line 146
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.adjoin_quotient_coordinates line 163
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_coordinate_transcendence_basis line 174
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_prime_quotient_coordinate_basis line 186
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficient_nonZeroDivisors_disjoint line 203
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficient_localization_prime_height line 216
  14. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficientLocalizationLocalEquiv line 229
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.kernel_isMaximal_of_algebraic_field line 248
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coefficient_localization_isMaximal line 256
  17. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateFractionAlgebra line 267
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateFractionAlgebra_algebraMap line 274
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.transcendenceBasis_isAlgebraic_coordinateFraction line 284
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateFraction_aeval_comp_map line 296
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateFraction_kernel_isMaximal line 316
  22. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit line 339
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_C line 345
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_X_mem line 350
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_X_compl line 355
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_symm_C line 360
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_symm_X_compl line 372
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.aeval_coordinateSplit_symm line 378
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_comap_coefficients_eq_bot line 392
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_comap_coefficients_eq_bot_of_fractionField line 409
  31. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplitLocalEquiv line 420
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.totalDegree_coordinateSplit_le line 427
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.totalDegree_localized_coordinateSplit_le line 462
  34. def OAI.SiegelZeros.WeightedTorusJets.Geometry.componentCoordinate line 471
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.aeval_componentCoordinate line 477
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.ker_aeval_componentCoordinate line 485
  37. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_prime_eq_evaluation_kernel line 495
  38. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coordinateSplit_localized_prime_isMaximal line 510