OAI/NumberTheory/Jacobsthal/Siegel/Homogenize.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.homogenize line 65
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogenize_isHomogeneous line 69
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.dehomogenize_homogenize line 81
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogenize_totalDegree line 87
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.map_span_homogenize line 96
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.span_homogenize_isHomogeneous line 108
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneous_eval₂_mul line 115
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.eval₂_homogenize line 128
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.polynomial_eval₂_homogenize line 152
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneMap_homogenize line 168
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogenize_mem_coneIdeal line 186
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.map_coneIdeal_dehomogenize line 191
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.conePolynomialMap_homogenize line 206
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.conePolynomialMap_padded_homogenize line 218
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_length_eq_of_flat_local_extension line 229
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_length_local_polynomial line 243
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_polynomial_parameter_isUnit line 255
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.span_range_mul_units line 274
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_length_eq_of_ringEquiv line 279
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.radical_map_eq_maximal_of_radical_eq line 285
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mem_minimalPrimes_of_local_radical line 296
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.local_polynomial_scaled_span line 308
  23. def OAI.Erdos970.WeightedTorusJets.Geometry.paddedHomogenizedIdeal line 328
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.paddedHomogenizedIdeal_le_coneIdeal line 332
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.paddedHomogenizedIdeal_isHomogeneous line 341
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneLocalEquiv_padded_ideal line 357
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.cone_padded_quotient_length line 396
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.cone_padded_local_radical line 415
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.coneIdeal_mem_minimalPrimes_padded line 450
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.padded_homogenize_isHomogeneous_of_le line 466
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.padded_homogenize_totalDegree_le line 473