OAI/NumberTheory/Jacobsthal/Siegel/DegreeMap.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMap line 25
  2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMap_surjective line 33
  3. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMul line 38
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMul_injective line 49
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.homogeneous_mem_sup_span_iff line 57
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.homogeneous_mem_sup_span_iff_of_lt line 81
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.ker_degreeMap_eq_range_degreeMul line 98
  8. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeCokernelEquiv line 127
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeCokernelEquiv_mk line 136
  10. instance OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreePiece_finite line 143
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span_add line 147
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMap_injective_of_lt line 158
  13. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeEquivOfLt line 176
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span line 183
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span_add_finrank line 197
  16. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.quotientMulColon line 223
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.quotientMulColon_mk line 232
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.quotientMulColon_injective line 236
  19. def OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMulColon line 250
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMulColon_injective line 263
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreeMulColon_comp_degreeMap line 270
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.range_degreeMulColon line 278
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.colon_isHomogeneous line 284
  24. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_sup_span_add_colon line 298
  25. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.degreePiece_eq_bot_of_variables_mem line 320
  26. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_eq_zero_of_variables_mem line 335
  27. theorem OAI.Erdos970.WeightedTorusJets.Geometry.HilbertRational.polynomial line 352
  28. theorem OAI.Erdos970.WeightedTorusJets.Geometry.HilbertRational.add line 355
  29. theorem OAI.Erdos970.WeightedTorusJets.Geometry.HilbertRational.X_mul line 367
  30. theorem OAI.Erdos970.WeightedTorusJets.Geometry.HilbertRational.of_eq_add_X_mul_self line 376
  31. theorem OAI.Erdos970.WeightedTorusJets.Geometry.HilbertRational.exists_mul_invOneSubPow line 385
  32. theorem OAI.Erdos970.WeightedTorusJets.Geometry.hilbertRational_of_noetherian_recurrence line 396
  33. theorem OAI.Erdos970.Polynomial.coeff_hilbertPoly_succ_top line 426
  34. theorem OAI.Erdos970.Polynomial.natDegree_hilbertPoly_succ_le line 434
  35. theorem OAI.Erdos970.Polynomial.natDegree_hilbertPoly_succ_of_eval_one_ne_zero line 441
  36. theorem OAI.Erdos970.Polynomial.leadingCoeff_hilbertPoly_succ_of_eval_one_ne_zero line 447
  37. theorem OAI.Erdos970.Polynomial.factorial_mul_leadingCoeff_hilbertPoly_succ line 453
  38. theorem OAI.Erdos970.Polynomial.hilbertPoly_mul_one_sub_X_pow line 460
  39. theorem OAI.Erdos970.Polynomial.factorial_mul_leadingCoeff_hilbertPoly_hypersurface line 469