OAI/RingTheory/Multiplicity/PartialLaurentTotalDegree.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.PartialLaurent.totalDegreeNat line 17
  2. def OAI.Lech.PartialLaurent.totalDegreeInt line 21
  3. abbrev OAI.Lech.PartialLaurent.polyGrade line 25
  4. abbrev OAI.Lech.PartialLaurent.laurentGrade line 26
  5. lemma OAI.Lech.PartialLaurent.homogeneous_eq_grade line 27
  6. lemma OAI.Lech.PartialLaurent.total_fromNat line 30
  7. lemma OAI.Lech.PartialLaurent.total_indicator line 33
  8. lemma OAI.Lech.PartialLaurent.denominator_homogeneous line 36
  9. lemma OAI.Lech.PartialLaurent.algebraMap_homogeneous line 39
  10. lemma OAI.Lech.PartialLaurent.algebraMap_homogeneous_iff line 46
  11. def OAI.Lech.PartialLaurent.zeroDegree line 60
  12. abbrev OAI.Lech.PartialLaurent.projectiveChart line 68
  13. def OAI.Lech.PartialLaurent.homogeneousToLaurent line 69
  14. lemma OAI.Lech.PartialLaurent.homogeneousToLaurent_injective line 73
  15. lemma OAI.Lech.PartialLaurent.inverse_denominator line 77
  16. lemma OAI.Lech.PartialLaurent.total_negative_indicator line 85
  17. lemma OAI.Lech.PartialLaurent.inverse_denominator_homogeneous line 89
  18. lemma OAI.Lech.PartialLaurent.homogeneousToLaurent_mk line 96
  19. lemma OAI.Lech.PartialLaurent.homogeneousToLaurent_mem line 108
  20. def OAI.Lech.PartialLaurent.projectiveToZero line 117
  21. lemma OAI.Lech.PartialLaurent.projectiveToZero_surjective line 120
  22. def OAI.Lech.PartialLaurent.projectiveEquiv line 135
  23. lemma OAI.Lech.PartialLaurent.restrict_homogeneous line 146
  24. def OAI.Lech.PartialLaurent.homogeneousRestrict line 155
  25. def OAI.Lech.PartialLaurent.chartExponent line 167
  26. lemma OAI.Lech.PartialLaurent.chartExponent_degree line 174
  27. lemma OAI.Lech.PartialLaurent.chartMonomial_mul line 177
  28. lemma OAI.Lech.PartialLaurent.chartMonomial_inverse line 181
  29. lemma OAI.Lech.PartialLaurent.chartMonomial_homogeneous line 185
  30. def OAI.Lech.PartialLaurent.twistTrivialization line 191
  31. def OAI.Lech.PartialLaurent.degreeInclusion line 215
  32. lemma OAI.Lech.PartialLaurent.homogeneousEquiv_symm_single line 219
  33. def OAI.Lech.PartialLaurent.coefficientChartRestrict line 227
  34. lemma OAI.Lech.PartialLaurent.homogeneousEquiv_restrict_symm line 238
  35. lemma OAI.Lech.PartialLaurent.homogeneousEquiv_restrict line 254
  36. lemma OAI.Lech.PartialLaurent.exponent_allowed_iff line 263
  37. abbrev OAI.Lech.ActualCech.Row line 284
  38. def OAI.Lech.ActualCech.delta line 287
  39. def OAI.Lech.ActualCech.extra line 297
  40. lemma OAI.Lech.ActualCech.delete_insert_zero line 302
  41. lemma OAI.Lech.ActualCech.delete_insert_succ line 306
  42. lemma OAI.Lech.ActualCech.extra_delta line 314
  43. lemma OAI.Lech.ActualCech.extra_delta_zero line 323
  44. lemma OAI.Lech.ActualCech.delta_square line 331
  45. abbrev OAI.Lech.ActualCech.Cochains line 353
  46. def OAI.Lech.ActualCech.d line 355
  47. lemma OAI.Lech.ActualCech.d_apply line 357
  48. def OAI.Lech.ActualCech.Allowed line 362
  49. def OAI.Lech.ActualCech.homogeneous line 365
  50. lemma OAI.Lech.ActualCech.d_mem line 371
  51. lemma OAI.Lech.ActualCech.exists_nonneg line 387
  52. def OAI.Lech.ActualCech.chosen line 397
  53. lemma OAI.Lech.ActualCech.chosen_nonneg line 399
  54. def OAI.Lech.ActualCech.contraction line 405
  55. lemma OAI.Lech.ActualCech.contraction_apply line 408
  56. lemma OAI.Lech.ActualCech.contraction_mem line 421
  57. lemma OAI.Lech.ActualCech.contraction_identity line 446
  58. theorem OAI.Lech.ActualCech.exact_nonnegative line 456