OAI/NumberTheory/Jacobsthal/Siegel/ConeMap.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.coneMap line 18
  2. def OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal line 23
  3. def OAI.Erdos970.WeightedTorusJets.Geometry.coneDehomogenize line 26
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneMap_X_none line 30
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneMap_X_some line 34
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal_isPrime line 39
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.X_none_not_mem_coneIdeal line 42
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.eval_one_coneMap line 47
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.map_coneIdeal_dehomogenize_le line 56
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomial_local_coefficient_prime_map line 74
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomial_coefficient_denominators_disjoint line 86
  12. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientPolyEquiv line 94
  13. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientEquiv line 115
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientEquiv_polynomial line 121
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientEquiv_algebraMap line 129
  16. def OAI.Erdos970.WeightedTorusJets.Geometry.conePolynomialMap line 145
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.conePolynomialMap_X_none line 150
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.conePolynomialMap_X_some line 154
  19. def OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayForward line 164
  20. def OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayInverseCoefficients line 171
  21. def OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayBackward line 175
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayForward_algebraMap line 181
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayBackward_algebraMap line 185
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayForward_invSelf line 190
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayForward_comp_backward line 201
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayBackward_comp_forward line 221
  27. def OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayEquiv line 239
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneAwayEquiv_algebraMap line 243
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal_eq_comap_polynomial line 255
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_X_powers_disjoint line 272
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomialAwayPrime_isPrime line 282
  32. def OAI.Erdos970.WeightedTorusJets.Geometry.conePolynomialLocalEquiv line 290
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.conePolynomialLocalEquiv_algebraMap line 329
  34. def OAI.Erdos970.WeightedTorusJets.Geometry.coneLocalEquiv line 355
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneLocalEquiv_algebraMap line 362
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_height_map_C line 385
  37. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_polynomial_prime_ringKrullDim line 397
  38. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal_height line 411