OAI/RingTheory/Multiplicity/LechSignedUnit.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.signedUnitProduct line 17
  2. lemma OAI.Lech.RootInvariants.chartTransition_unit_value line 36
  3. lemma OAI.Lech.RootInvariants.commonWeight_product line 46
  4. lemma OAI.Lech.RootInvariants.chartTransition_product line 57
  5. def OAI.Lech.RootInvariants.coordinateTransition line 70
  6. lemma OAI.Lech.RootInvariants.coordinateTransition_val line 74
  7. def OAI.Lech.LineBasisExtension.included line 89
  8. lemma OAI.Lech.LineBasisExtension.included_tmul line 91
  9. lemma OAI.Lech.LineBasisExtension.included_smul line 92
  10. lemma OAI.Lech.LineBasisExtension.extend_one line 97
  11. lemma OAI.Lech.LineBasisExtension.extend_coefficient line 106
  12. lemma OAI.Lech.LineBasisExtension.coefficients_in_basis line 111
  13. def OAI.Lech.LineBasisExtension.coordinates line 115
  14. lemma OAI.Lech.LineBasisExtension.coordinates_apply line 117
  15. instance OAI.Lech.RootChartAtlas.gridRootAlgebra line 132
  16. lemma OAI.Lech.RootChartAtlas.gridRootAlgebraMap line 134
  17. lemma OAI.Lech.RootChartAtlas.chartToGrid_from line 136
  18. def OAI.Lech.RootChartAtlas.chartToGridD line 141
  19. lemma OAI.Lech.RootChartAtlas.chartToGridD_apply line 143
  20. lemma OAI.Lech.RootChartAtlas.chartToGrid_injective line 145
  21. lemma OAI.Lech.RootChartAtlas.gridRootAlgebra_injective line 147
  22. def OAI.Lech.RootChartAtlas.gridBasis line 153
  23. lemma OAI.Lech.RootChartAtlas.gridCoordinateTransition line 156
  24. def OAI.Lech.RootInvariants.commonInclusion line 180
  25. lemma OAI.Lech.RootInvariants.commonBasis_from line 184
  26. lemma OAI.Lech.RootInvariants.commonInclusion_coordinate line 194
  27. def OAI.Lech.ProductLaurent.monomialHom line 214
  28. lemma OAI.Lech.ProductLaurent.monomialUnit_zsmul line 218
  29. lemma OAI.Lech.ProductLaurent.monomialUnit_sum line 221
  30. lemma OAI.Lech.ProductLaurent.signedProduct line 226
  31. lemma OAI.Lech.RootChartAtlas.gridTransition line 259
  32. def OAI.Lech.RootChartAtlas.gridInclusion line 274
  33. def OAI.Lech.RootChartAtlas.gridCoefficient line 277
  34. lemma OAI.Lech.RootChartAtlas.gridCoefficient_apply line 281
  35. theorem OAI.Lech.RootChartAtlas.gridCoefficient_range line 293
  36. lemma OAI.Lech.RootInvariants.line_finitePresentation line 319
  37. lemma OAI.Lech.RootInvariants.line_flat line 326
  38. lemma OAI.Lech.RootInvariants.line_projective line 333
  39. lemma OAI.Lech.RootInvariants.line_rankAtStalk line 339
  40. def OAI.Lech.LocalizationImageCover.localMap line 360
  41. lemma OAI.Lech.LocalizationImageCover.localMap_from line 364
  42. lemma OAI.Lech.LocalizationImageCover.localMap_clear line 369
  43. theorem OAI.Lech.LocalizationImageCover.globalImage_iff line 382
  44. lemma OAI.Lech.LocalizationImageCover.global_injective line 401
  45. lemma OAI.Lech.AlternatingCech.empty_mem_of_singletons line 421