OAI/NumberTheory/SiegelZeros/Structure/DegreeMap.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMap line 21
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMap_surjective line 29
  3. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMul line 34
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMul_injective line 45
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.homogeneous_mem_sup_span_iff line 53
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.homogeneous_mem_sup_span_iff_of_lt line 77
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.ker_degreeMap_eq_range_degreeMul line 94
  8. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeCokernelEquiv line 123
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeCokernelEquiv_mk line 132
  10. instance OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreePiece_finite line 139
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span_add line 143
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMap_injective_of_lt line 154
  13. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeEquivOfLt line 172
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span line 179
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span_add_finrank line 193
  16. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.quotientMulColon line 219
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.quotientMulColon_mk line 228
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.quotientMulColon_injective line 232
  19. def OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMulColon line 246
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMulColon_injective line 259
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreeMulColon_comp_degreeMap line 266
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.range_degreeMulColon line 274
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.colon_isHomogeneous line 280
  24. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span_add_colon line 294
  25. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.degreePiece_eq_bot_of_variables_mem line 316
  26. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_eq_zero_of_variables_mem line 331
  27. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.HilbertRational.polynomial line 348
  28. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.HilbertRational.add line 351
  29. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.HilbertRational.X_mul line 363
  30. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.HilbertRational.of_eq_add_X_mul_self line 372
  31. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.HilbertRational.exists_mul_invOneSubPow line 381
  32. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.hilbertRational_of_noetherian_recurrence line 392
  33. theorem OAI.SiegelZeros.Polynomial.coeff_hilbertPoly_succ_top line 422
  34. theorem OAI.SiegelZeros.Polynomial.natDegree_hilbertPoly_succ_le line 430
  35. theorem OAI.SiegelZeros.Polynomial.natDegree_hilbertPoly_succ_of_eval_one_ne_zero line 437
  36. theorem OAI.SiegelZeros.Polynomial.leadingCoeff_hilbertPoly_succ_of_eval_one_ne_zero line 443
  37. theorem OAI.SiegelZeros.Polynomial.factorial_mul_leadingCoeff_hilbertPoly_succ line 449
  38. theorem OAI.SiegelZeros.Polynomial.hilbertPoly_mul_one_sub_X_pow line 456
  39. theorem OAI.SiegelZeros.Polynomial.factorial_mul_leadingCoeff_hilbertPoly_hypersurface line 465