OAI/NumberTheory/SiegelZeros/Hilbert/HomogeneousDeformation.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.homogeneousDeformation line 18
  2. theorem OAI.SiegelZeros.WeightedTorusJets.map_homogeneousComponent line 22
  3. theorem OAI.SiegelZeros.WeightedTorusJets.polynomialDeformation_at_one line 28
  4. theorem OAI.SiegelZeros.WeightedTorusJets.homogeneousDeformation_at_one line 32
  5. def OAI.SiegelZeros.WeightedTorusJets.macaulayColumn line 37
  6. def OAI.SiegelZeros.WeightedTorusJets.macaulayMap line 45
  7. def OAI.SiegelZeros.WeightedTorusJets.macaulayMatrix line 51
  8. theorem OAI.SiegelZeros.WeightedTorusJets.macaulayMatrix_map line 56
  9. theorem OAI.SiegelZeros.WeightedTorusJets.deformed_macaulay_at_one line 64
  10. def OAI.SiegelZeros.WeightedTorusJets.monomialDegreeFintype line 76
  11. def OAI.SiegelZeros.WeightedTorusJets.monomialSourceFintype line 80
  12. def OAI.SiegelZeros.WeightedTorusJets.homogeneousMonomialBasis line 87
  13. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreePiece line 103
  14. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreePresentation line 107
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreePresentation_surjective line 111
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.ker_degreePresentation line 115
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_eq_sub_finrank_range line 122
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.homogeneousComponent_mul_of_le line 141
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.homogeneousComponent_mul_of_lt line 150
  20. theorem OAI.SiegelZeros.WeightedTorusJets.macaulayMap_range_eq_ideal_slice line 164
  21. theorem OAI.SiegelZeros.WeightedTorusJets.toMatrix_macaulayMap line 218
  22. theorem OAI.SiegelZeros.WeightedTorusJets.macaulayMatrix_rank_eq_finrank_range line 230
  23. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_degreePiece_span_eq_sub_macaulayMatrix_rank line 240
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_row_minor_det_ne_zero line 255
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_rank_minor line 280
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rank_specialization_le line 304
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rank_polynomial_eval_le line 326
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_homogeneousSubmodule line 334
  29. theorem OAI.SiegelZeros.WeightedTorusJets.deformed_macaulay_generic_rank_ge line 349
  30. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_degreePiece_deformed_le_pure_powers line 367
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneous_quotient_coeLinearMap_injective line 397
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_finrank_le_sum_homogeneous_images line 443
  33. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_finrank_le_of_homogeneous_image_finrank_le line 481
  34. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularIdeal line 529
  35. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.mem_rectangularIdeal line 533
  36. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularIdeal_restrictScalars line 544
  37. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.isCompl_restrictSupport_compl line 551
  38. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularQuotientEquiv line 559
  39. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularExponentEquiv line 570
  40. def OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularQuotientBasis line 577
  41. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_rectangularQuotient line 582
  42. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.homogeneous_mem_rectangularIdeal line 590
  43. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangular_homogeneous_image_eq_bot line 606
  44. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularIdeal_isHomogeneous line 621
  45. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.quotient_finrank_le_prod_of_homogeneous_image_le_rectangular line 628