OAI/RingTheory/Multiplicity/LechHomogeneousEval.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.homogeneous_eval_scale line 22
  2. lemma OAI.Lech.ProjectiveCoefficientChart.coordinate_self line 45
  3. lemma OAI.Lech.ProjectiveCoefficientChart.forward_coefficient line 49
  4. lemma OAI.Lech.ProjectiveCoefficientChart.coordinate_mul line 56
  5. lemma OAI.Lech.ProjectiveCoefficientChart.inclusion_forward_evaluate line 61
  6. lemma OAI.Lech.ProjectiveCoefficientChart.homogeneous_identity line 71
  7. lemma OAI.Lech.ProjectiveCoefficientChart.forward_backward line 89
  8. def OAI.Lech.ProjectiveCoefficientChart.equiv line 101
  9. abbrev OAI.Lech.ProjectiveCoefficientChart.Overlap line 113
  10. def OAI.Lech.ProjectiveCoefficientChart.overlapMap line 114
  11. def OAI.Lech.ProjectiveCoefficientChart.overlapChartAlgebra line 116
  12. def OAI.Lech.ProjectiveCoefficientChart.overlapCoefficientMap line 118
  13. def OAI.Lech.ProjectiveCoefficientChart.overlapCoefficientAlgebra line 120
  14. lemma OAI.Lech.ProjectiveCoefficientChart.backward_localizationElem line 122
  15. lemma OAI.Lech.ProjectiveCoefficientChart.equiv_evaluate_localizationElem line 125
  16. theorem OAI.Lech.ProjectiveCoefficientChart.overlap_isLocalization line 132
  17. lemma OAI.Lech.ProductSourceCover.chartScalar_coefficient_unit line 157
  18. def OAI.Lech.ProductSourceCover.localizedChart line 166
  19. lemma OAI.Lech.ProductSourceCover.localizedChart_algebraMap line 170
  20. lemma OAI.Lech.ProductSourceCover.chartScalar_injective line 173
  21. lemma OAI.Lech.ProductSourceCover.localizedChart_injective line 175
  22. lemma OAI.Lech.ProductSourceCover.twistExponent_add line 187
  23. lemma OAI.Lech.ProductSourceCover.twistExponent_level line 191
  24. lemma OAI.Lech.ProductSourceCover.monomialUnit_nsmul line 195
  25. lemma OAI.Lech.ProductSourceCover.chartLine_level line 200
  26. def OAI.Lech.ProductSourceCover.localizedLine line 210
  27. lemma OAI.Lech.ProductSourceCover.localizedLine_apply line 214
  28. lemma OAI.Lech.ProductSourceCover.targetCoeff_chart line 218
  29. lemma OAI.Lech.ProductSourceCover.localizedLine_mem line 223
  30. lemma OAI.Lech.ProductSourceCover.localizedLine_injective line 238
  31. theorem OAI.Lech.ProductSourceCover.localizedLine_range line 246
  32. def OAI.Lech.ProductSourceCover.localizedLineEquiv line 275
  33. def OAI.Lech.ProductSourceCover.targetUnit line 285
  34. lemma OAI.Lech.ProductSourceCover.targetUnit_val line 286
  35. def OAI.Lech.ProductSourceCover.gridTarget line 291
  36. lemma OAI.Lech.ProductSourceCover.gridTarget_coefficient line 293
  37. lemma OAI.Lech.ProductSourceCover.targetUnit_chart line 298
  38. lemma OAI.Lech.ProductSourceCover.ratio_rescale line 306
  39. theorem OAI.Lech.ProductSourceCover.localizedChart_target line 314
  40. instance OAI.Lech.ProductSourceCover.gridTargetAlgebra line 328
  41. instance OAI.Lech.ProductSourceCover.gridTargetTower line 330
  42. def OAI.Lech.ProductSourceCover.localizedChartA line 333
  43. lemma OAI.Lech.ProductSourceCover.grid_mul_mem line 342
  44. lemma OAI.Lech.ProductSourceCover.grid_one_mem line 358
  45. lemma OAI.Lech.ProductSourceCover.grid_zero_pow_mem line 363
  46. def OAI.Lech.ProductSourceCover.targetProduct line 369
  47. lemma OAI.Lech.ProductSourceCover.targetProduct_map line 371
  48. lemma OAI.Lech.ProductSourceCover.targetProduct_relation line 377
  49. def OAI.Lech.ProductSourceCover.targetProductUnit line 380
  50. lemma OAI.Lech.ProductSourceCover.targetProductUnit_val line 382
  51. lemma OAI.Lech.ProductSourceCover.targetProductUnit_inv_mem line 386
  52. structure OAI.Lech.UniversalSplitting.Data line 406
  53. theorem OAI.Lech.UniversalSplitting.exists_data line 419
  54. theorem OAI.Lech.UniversalSplitting.exists_data_all line 515
  55. lemma OAI.Lech.UniversalSplitting.Data.hom_ext line 534
  56. def OAI.Lech.UniversalSplitting.Data.baseChange line 544
  57. lemma OAI.Lech.UniversalSplitting.Data.finite line 578
  58. lemma OAI.Lech.UniversalSplitting.Data.free line 581
  59. lemma OAI.Lech.UniversalSplitting.Data.flat line 584