OAI/RingTheory/Multiplicity/RootChartAtlasGlobalCoefficient.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.RootChartAtlas.globalCoefficient line 31
  2. lemma OAI.Lech.RootChartAtlas.gridCoefficient_from line 35
  3. lemma OAI.Lech.RootChartAtlas.globalCoefficient_local line 42
  4. theorem OAI.Lech.RootChartAtlas.globalCoefficient_range line 63
  5. lemma OAI.Lech.RootChartAtlas.globalCoefficient_injective line 73
  6. abbrev OAI.Lech.PrimitiveRootModule.chart line 87
  7. def OAI.Lech.PrimitiveRootModule.coordinate line 89
  8. lemma OAI.Lech.PrimitiveRootModule.eval_coordinate line 91
  9. def OAI.Lech.PrimitiveRootModule.valueUnit line 102
  10. lemma OAI.Lech.PrimitiveRootModule.valueUnit_val line 105
  11. lemma OAI.Lech.PrimitiveRootModule.eval_valueUnit line 108
  12. def OAI.Lech.PrimitiveRootModule.splitting line 111
  13. abbrev OAI.Lech.PrimitiveRootModule.module line 123
  14. lemma OAI.Lech.PrimitiveRootModule.finite_projective line 126
  15. lemma OAI.Lech.PrimitiveRootModule.rankAtStalk line 133
  16. def OAI.Lech.PrimitiveRootModule.tensorEquiv line 141
  17. def OAI.Lech.RootChartAtlas.globalCoefficientA line 166
  18. lemma OAI.Lech.RootChartAtlas.globalCoefficientA_range line 170
  19. lemma OAI.Lech.RootChartAtlas.globalCoefficientA_injective line 173
  20. lemma OAI.Lech.RootChartAtlas.grid_smul_mem line 177
  21. def OAI.Lech.ProductSourceCover.sectionModule line 192
  22. lemma OAI.Lech.ProductSourceCover.sectionModule_mem line 203
  23. def OAI.Lech.RootChartAtlas.globalSectionMap line 220
  24. def OAI.Lech.RootChartAtlas.globalSectionEquiv line 226
  25. lemma OAI.Lech.RootChartAtlas.section_finitePresentation line 235
  26. lemma OAI.Lech.RootChartAtlas.section_projective line 240
  27. lemma OAI.Lech.RootChartAtlas.section_rank line 245
  28. theorem OAI.Lech.ProductSourceCover.sectionModule_properties line 258
  29. lemma OAI.Lech.ProductSourceCover.grid_clear_target line 283
  30. theorem OAI.Lech.ProductSourceCover.grid_localization_iff line 304
  31. def OAI.Lech.ProductSourceCover.overlapModule line 322
  32. def OAI.Lech.ProductSourceCover.restriction line 337
  33. lemma OAI.Lech.ProductSourceCover.restriction_injective line 340
  34. lemma OAI.Lech.ProductSourceCover.inverse_mem_overlap line 342
  35. instance OAI.Lech.ProductSourceCover.restriction_localized line 359
  36. abbrev OAI.Lech.ProductSourceCover.OverlapRing line 393
  37. def OAI.Lech.ProductSourceCover.overlapBaseChange line 402
  38. lemma OAI.Lech.ProductSourceCover.overlapBaseChange_one line 407
  39. theorem OAI.Lech.ProductSourceCover.overlapModule_properties line 413
  40. def OAI.Lech.ProductSourceCover.projectiveRemainder line 434
  41. lemma OAI.Lech.ProductSourceCover.projectiveRemainder_homogeneous line 435
  42. lemma OAI.Lech.ProductSourceCover.projectiveRemainder_product line 439
  43. lemma OAI.Lech.ProductSourceCover.projectiveRemainder_evaluate line 442
  44. abbrev OAI.Lech.ProductSourceCover.HomogeneousOverlapRing line 449
  45. instance OAI.Lech.ProductSourceCover.homogeneousOverlapAlgebra line 451
  46. lemma OAI.Lech.ProductSourceCover.homogeneousOverlap_isLocalization line 454
  47. def OAI.Lech.ProductSourceCover.homogeneousOverlapBaseChange line 473
  48. lemma OAI.Lech.ProductSourceCover.homogeneousOverlapBaseChange_one line 479
  49. theorem OAI.Lech.ProductSourceCover.homogeneousOverlapModule_properties line 484