OAI/NumberTheory/SiegelZeros/Structure/Homogenize.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.homogenize line 33
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogenize_isHomogeneous line 37
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.dehomogenize_homogenize line 49
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogenize_totalDegree line 55
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.map_span_homogenize line 64
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.span_homogenize_isHomogeneous line 76
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneous_eval₂_mul line 83
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.eval₂_homogenize line 96
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.polynomial_eval₂_homogenize line 120
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneMap_homogenize line 136
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogenize_mem_coneIdeal line 154
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.map_coneIdeal_dehomogenize line 159
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.conePolynomialMap_homogenize line 174
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.conePolynomialMap_padded_homogenize line 186
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_length_eq_of_flat_local_extension line 197
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_length_local_polynomial line 211
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_polynomial_parameter_isUnit line 223
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.span_range_mul_units line 242
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_length_eq_of_ringEquiv line 247
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.radical_map_eq_maximal_of_radical_eq line 253
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mem_minimalPrimes_of_local_radical line 264
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.local_polynomial_scaled_span line 276
  23. def OAI.SiegelZeros.WeightedTorusJets.Geometry.paddedHomogenizedIdeal line 296
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.paddedHomogenizedIdeal_le_coneIdeal line 300
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.paddedHomogenizedIdeal_isHomogeneous line 309
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneLocalEquiv_padded_ideal line 325
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.cone_padded_quotient_length line 364
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.cone_padded_local_radical line 383
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.coneIdeal_mem_minimalPrimes_padded line 418
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.padded_homogenize_isHomogeneous_of_le line 434
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.padded_homogenize_totalDegree_le line 441