OAI/NumberTheory/Jacobsthal/Siegel/HomogeneousDeformation.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.homogeneousDeformation line 21
  2. theorem OAI.Erdos970.WeightedTorusJets.map_homogeneousComponent line 25
  3. theorem OAI.Erdos970.WeightedTorusJets.polynomialDeformation_at_one line 31
  4. theorem OAI.Erdos970.WeightedTorusJets.homogeneousDeformation_at_one line 35
  5. def OAI.Erdos970.WeightedTorusJets.macaulayColumn line 40
  6. def OAI.Erdos970.WeightedTorusJets.macaulayMap line 48
  7. def OAI.Erdos970.WeightedTorusJets.macaulayMatrix line 54
  8. theorem OAI.Erdos970.WeightedTorusJets.macaulayMatrix_map line 59
  9. theorem OAI.Erdos970.WeightedTorusJets.deformed_macaulay_at_one line 67
  10. def OAI.Erdos970.WeightedTorusJets.monomialDegreeFintype line 79
  11. def OAI.Erdos970.WeightedTorusJets.monomialSourceFintype line 83
  12. def OAI.Erdos970.WeightedTorusJets.homogeneousMonomialBasis line 90
  13. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreePiece line 106
  14. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreePresentation line 110
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreePresentation_surjective line 114
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.ker_degreePresentation line 118
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_eq_sub_finrank_range line 125
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.homogeneousComponent_mul_of_le line 144
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.homogeneousComponent_mul_of_lt line 153
  20. theorem OAI.Erdos970.WeightedTorusJets.macaulayMap_range_eq_ideal_slice line 167
  21. theorem OAI.Erdos970.WeightedTorusJets.toMatrix_macaulayMap line 221
  22. theorem OAI.Erdos970.WeightedTorusJets.macaulayMatrix_rank_eq_finrank_range line 233
  23. theorem OAI.Erdos970.WeightedTorusJets.finrank_degreePiece_span_eq_sub_macaulayMatrix_rank line 243
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_row_minor_det_ne_zero line 258
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_rank_minor line 283
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rank_specialization_le line 307
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rank_polynomial_eval_le line 329
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_homogeneousSubmodule line 337
  29. theorem OAI.Erdos970.WeightedTorusJets.deformed_macaulay_generic_rank_ge line 352
  30. theorem OAI.Erdos970.WeightedTorusJets.finrank_degreePiece_deformed_le_pure_powers line 370
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneous_quotient_coeLinearMap_injective line 401
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_finrank_le_sum_homogeneous_images line 447
  33. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_finrank_le_of_homogeneous_image_finrank_le line 485
  34. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularIdeal line 533
  35. theorem OAI.Erdos970.WeightedTorusJets.Geometry.mem_rectangularIdeal line 537
  36. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularIdeal_restrictScalars line 548
  37. theorem OAI.Erdos970.WeightedTorusJets.Geometry.isCompl_restrictSupport_compl line 555
  38. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularQuotientEquiv line 563
  39. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularExponentEquiv line 574
  40. def OAI.Erdos970.WeightedTorusJets.Geometry.rectangularQuotientBasis line 581
  41. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_rectangularQuotient line 586
  42. theorem OAI.Erdos970.WeightedTorusJets.Geometry.homogeneous_mem_rectangularIdeal line 594
  43. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangular_homogeneous_image_eq_bot line 610
  44. theorem OAI.Erdos970.WeightedTorusJets.Geometry.rectangularIdeal_isHomogeneous line 625
  45. theorem OAI.Erdos970.WeightedTorusJets.Geometry.quotient_finrank_le_prod_of_homogeneous_image_le_rectangular line 632