OAI/RingTheory/Multiplicity/PrincipalCoverRegularRegularMap.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.PrincipalCoverRegular.regular_map line 19
  2. theorem OAI.Lech.PrincipalCoverRegular.regular_of_cover line 24
  3. abbrev OAI.Lech.ProductLaurent.Exponent line 46
  4. abbrev OAI.Lech.ProductLaurent.Ring line 47
  5. def OAI.Lech.ProductLaurent.signedExponent line 49
  6. lemma OAI.Lech.ProductLaurent.signedExponent_apply line 61
  7. lemma OAI.Lech.ProductLaurent.signedExponent_injective line 63
  8. def OAI.Lech.ProductLaurent.chartMap line 70
  9. lemma OAI.Lech.ProductLaurent.chartMap_injective line 72
  10. lemma OAI.Lech.ProductLaurent.chartMap_monomial line 74
  11. def OAI.Lech.ProductLaurent.monomialUnit line 78
  12. abbrev OAI.Lech.ProductLaurent.variableUnit line 83
  13. lemma OAI.Lech.ProductLaurent.monomialUnit_add line 84
  14. lemma OAI.Lech.ProductLaurent.monomialUnit_neg line 88
  15. lemma OAI.Lech.ProductLaurent.chartMap_X line 91
  16. def OAI.Lech.ProductLaurent.chartUnit line 103
  17. lemma OAI.Lech.ProductLaurent.chartMap_a line 104
  18. lemma OAI.Lech.ProductLaurent.chartMap_b line 110
  19. def OAI.Lech.ProductLaurent.binaryForm line 115
  20. lemma OAI.Lech.ProductLaurent.chartMap_factor line 116
  21. lemma OAI.Lech.ProductLaurent.chartUnit_inv line 127
  22. lemma OAI.Lech.ProductLaurent.chartMap_product line 133
  23. lemma OAI.Lech.ProductLaurent.chartMap_coefficient line 148
  24. def OAI.Lech.ProductLaurent.uniformExponent line 155
  25. lemma OAI.Lech.ProductLaurent.uniformExponent_apply line 156
  26. def OAI.Lech.ProductLaurent.naturalPart line 157
  27. lemma OAI.Lech.ProductLaurent.naturalPart_lift line 158
  28. def OAI.Lech.ProductLaurent.clearingBound line 163
  29. lemma OAI.Lech.ProductLaurent.clearingBound_nonneg line 165
  30. def OAI.Lech.ProductLaurent.clearedPolynomial line 177
  31. lemma OAI.Lech.ProductLaurent.clearing_identity line 180
  32. theorem OAI.Lech.ProductLaurent.chartMap_regular line 200
  33. lemma OAI.Lech.ProductLaurent.binaryForm_coefficient_regular line 216
  34. abbrev OAI.Lech.ProductSourceCover.Chart line 227
  35. abbrev OAI.Lech.ProductSourceCover.Exponent line 228
  36. abbrev OAI.Lech.ProductSourceCover.LaurentModule line 229
  37. def OAI.Lech.ProductSourceCover.allowed line 233
  38. def OAI.Lech.ProductSourceCover.sections line 235
  39. lemma OAI.Lech.ProductSourceCover.allowed_mono line 237
  40. lemma OAI.Lech.ProductSourceCover.sections_mono line 241
  41. def OAI.Lech.ProductSourceCover.badVertex line 246
  42. lemma OAI.Lech.ProductSourceCover.badVertex_false line 247
  43. lemma OAI.Lech.ProductSourceCover.badVertex_true line 249
  44. lemma OAI.Lech.ProductSourceCover.allowed_erase_bad line 251
  45. def OAI.Lech.ProductSourceCover.projector line 266
  46. lemma OAI.Lech.ProductSourceCover.projector_apply line 270
  47. lemma OAI.Lech.ProductSourceCover.projector_sum line 272
  48. lemma OAI.Lech.ProductSourceCover.projector_mem line 280
  49. theorem OAI.Lech.ProductSourceCover.augmented_acyclic line 293
  50. def OAI.Lech.ProductSourceCover.endpointVertex line 305
  51. lemma OAI.Lech.ProductSourceCover.endpointVertex_idem line 307
  52. def OAI.Lech.ProductSourceCover.endpointProjector line 310
  53. lemma OAI.Lech.ProductSourceCover.endpointProjector_apply line 315
  54. lemma OAI.Lech.ProductSourceCover.endpointProjector_sum line 318
  55. lemma OAI.Lech.ProductSourceCover.endpoint_allowed_carrier line 326
  56. lemma OAI.Lech.ProductSourceCover.endpointProjector_carrier line 368
  57. lemma OAI.Lech.ProductSourceCover.endpointProjector_zero line 379
  58. theorem OAI.Lech.ProductSourceCover.endpoint_acyclic line 406
  59. def OAI.Lech.ProductSourceCover.outlier line 423
  60. def OAI.Lech.ProductSourceCover.chosenOutlier line 425
  61. lemma OAI.Lech.ProductSourceCover.chosenOutlier_spec line 428
  62. lemma OAI.Lech.ProductSourceCover.chosenOutlier_none line 438
  63. def OAI.Lech.ProductSourceCover.central line 449
  64. lemma OAI.Lech.ProductSourceCover.central_iff line 451
  65. def OAI.Lech.ProductSourceCover.centralProjector line 469
  66. def OAI.Lech.ProductSourceCover.outlierProjector line 473
  67. lemma OAI.Lech.ProductSourceCover.centralProjector_apply line 477
  68. lemma OAI.Lech.ProductSourceCover.outlierProjector_apply line 479
  69. lemma OAI.Lech.ProductSourceCover.outlierProjector_sum line 481
  70. lemma OAI.Lech.ProductSourceCover.centralProjector_mem line 493
  71. lemma OAI.Lech.ProductSourceCover.centralProjector_idem line 502
  72. lemma OAI.Lech.ProductSourceCover.outlier_allowed_carrier line 509
  73. lemma OAI.Lech.ProductSourceCover.outlierProjector_carrier line 553
  74. lemma OAI.Lech.ProductSourceCover.outlierProjector_zero line 563