OAI/RingTheory/Multiplicity/LechFactorizationMap.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.factorization_map line 20
  2. abbrev OAI.Lech.RootChartAtlas.GridD line 45
  3. def OAI.Lech.RootChartAtlas.chartToGrid line 47
  4. lemma OAI.Lech.RootChartAtlas.chartToGrid_coordinate line 49
  5. def OAI.Lech.RootChartAtlas.factorUnit line 56
  6. lemma OAI.Lech.RootChartAtlas.factorization_grid line 58
  7. lemma OAI.Lech.RootChartAtlas.factor_selected line 73
  8. def OAI.Lech.RootChartAtlas.algebraPoint line 79
  9. lemma OAI.Lech.RootChartAtlas.algebraPoint_eq_factor line 81
  10. def OAI.Lech.RootChartAtlas.rescaleUnit line 94
  11. lemma OAI.Lech.RootChartAtlas.gridFactor_a line 96
  12. lemma OAI.Lech.RootChartAtlas.gridFactor_b line 104
  13. theorem OAI.Lech.RootChartAtlas.algebraPoint_independent line 114
  14. abbrev OAI.Lech.RootChartAtlas.D line 131
  15. abbrev OAI.Lech.RootChartAtlas.q line 132
  16. lemma OAI.Lech.RootChartAtlas.toH_chartFunction line 133
  17. lemma OAI.Lech.RootChartAtlas.coordinate_regular line 139
  18. lemma OAI.Lech.RootChartAtlas.localized_function_regular line 142
  19. theorem OAI.Lech.RootChartAtlas.chartFunction_regular line 165
  20. lemma OAI.Lech.StandardFactorCharts.coordinate_relation_ring line 181
  21. lemma OAI.Lech.StandardFactorCharts.selected_unit line 197
  22. def OAI.Lech.UnitSection.map line 216
  23. lemma OAI.Lech.UnitSection.compat line 219
  24. def OAI.Lech.UnitSection.equiv line 227
  25. def OAI.Lech.LocalLine.trivial line 247
  26. lemma OAI.Lech.LocalLine.trivial_tmul line 255
  27. def OAI.Lech.LocalLine.basisEquiv line 265
  28. lemma OAI.Lech.LocalLine.basisEquiv_apply line 271
  29. lemma OAI.Lech.LocalLine.section_relation line 277
  30. abbrev OAI.Lech.RootInvariants.chartModule line 309
  31. lemma OAI.Lech.RootInvariants.chart_tensor_compat line 312
  32. lemma OAI.Lech.RootInvariants.selected_tensor_unit line 325
  33. lemma OAI.Lech.RootInvariants.lineTensorEquiv_one line 340
  34. def OAI.Lech.RootInvariants.chartLineEquiv line 347
  35. lemma OAI.Lech.RootInvariants.chartLineEquiv_apply line 357
  36. lemma OAI.Lech.RootInvariants.chart_section_relation line 365
  37. lemma OAI.Lech.RootInvariants.weight_add line 407
  38. lemma OAI.Lech.RootInvariants.mul_mem line 411
  39. def OAI.Lech.RootInvariants.mulLinear line 430
  40. def OAI.Lech.RootInvariants.mulTensor line 441
  41. def OAI.Lech.RootInvariants.mulBaseSourceEquiv line 446
  42. lemma OAI.Lech.RootInvariants.mulBase_compat line 454
  43. lemma OAI.Lech.RootInvariants.mulTensor_bijective line 461
  44. def OAI.Lech.RootInvariants.lineMulEquiv line 474