OAI/NumberTheory/SiegelZeros/Structure/ConeMap.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneMap line 14
  2. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal line 19
  3. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneDehomogenize line 22
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneMap_X_none line 26
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneMap_X_some line 30
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal_isPrime line 35
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.X_none_not_mem_coneIdeal line 38
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.eval_one_coneMap line 43
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.map_coneIdeal_dehomogenize_le line 52
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomial_local_coefficient_prime_map line 70
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomial_coefficient_denominators_disjoint line 82
  12. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientPolyEquiv line 90
  13. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientEquiv line 111
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientEquiv_polynomial line 117
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialLocalCoefficientEquiv_algebraMap line 125
  16. def OAI.SiegelZeros.WeightedTorusJets.Geometry.conePolynomialMap line 141
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.conePolynomialMap_X_none line 146
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.conePolynomialMap_X_some line 150
  19. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayForward line 160
  20. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayInverseCoefficients line 167
  21. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayBackward line 171
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayForward_algebraMap line 177
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayBackward_algebraMap line 181
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayForward_invSelf line 186
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayForward_comp_backward line 197
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayBackward_comp_forward line 217
  27. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayEquiv line 235
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneAwayEquiv_algebraMap line 239
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal_eq_comap_polynomial line 251
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_X_powers_disjoint line 268
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomialAwayPrime_isPrime line 278
  32. def OAI.SiegelZeros.WeightedTorusJets.Geometry.conePolynomialLocalEquiv line 286
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.conePolynomialLocalEquiv_algebraMap line 325
  34. def OAI.SiegelZeros.WeightedTorusJets.Geometry.coneLocalEquiv line 351
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneLocalEquiv_algebraMap line 358
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_height_map_C line 381
  37. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_polynomial_prime_ringKrullDim line 393
  38. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal_height line 407