OAI/RingTheory/Multiplicity/UniversalFactorMapMapChart.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Lech.UniversalFactorMap.map_chart_selected line 34
2. def OAI.Lech.UniversalFactorMap.chartMap line 40
3. lemma OAI.Lech.UniversalFactorMap.chartMap_from line 45
4. lemma OAI.Lech.UniversalFactorMap.chartMap_unit line 56
5. lemma OAI.Lech.UniversalFactorMap.update_product line 65
6. lemma OAI.Lech.UniversalFactorMap.chartMap_coordinate line 78
7. lemma OAI.Lech.UniversalFactorMap.extend_map line 110
8. lemma OAI.Lech.UniversalFactorMap.chartMap_unique line 116
9. theorem OAI.Lech.UniversalFactorMap.chart_universal line 160
10. lemma OAI.Lech.UniversalFactorMap.normalizedRatio_rescale line 177
11. lemma OAI.Lech.UniversalFactorMap.denominator_rescale line 198
12. theorem OAI.Lech.UniversalFactorMap.map_rescale line 210
13. lemma OAI.Lech.ProductLinearChart.dehomogenize_factorization line 226
14. def OAI.Lech.ProductLinearChart.eval line 237
15. lemma OAI.Lech.ProductLinearChart.eval_a line 240
16. lemma OAI.Lech.ProductLinearChart.eval_b line 245
17. lemma OAI.Lech.ProductLinearChart.eval_product line 250
18. lemma OAI.Lech.ProductLinearChart.eval_coeff line 261
19. lemma OAI.Lech.ProductLinearChart.eval_self line 273
20. def OAI.Lech.ProductLinearChart.lift line 280
21. lemma OAI.Lech.ProductLinearChart.lift_from line 285
22. lemma OAI.Lech.ProductLinearChart.lift_denominator line 291
23. lemma OAI.Lech.ProductLinearChart.lift_target line 296
24. lemma OAI.Lech.ProductLinearChart.lift_X line 310
25. lemma OAI.Lech.ProductLinearChart.hom_ext line 317
26. abbrev OAI.Lech.RootChartAtlas.A line 338
27. abbrev OAI.Lech.RootChartAtlas.f line 339
28. abbrev OAI.Lech.RootChartAtlas.hn line 340
29. abbrev OAI.Lech.RootChartAtlas.L line 347
30. abbrev OAI.Lech.RootChartAtlas.H line 348
31. abbrev OAI.Lech.RootChartAtlas.coordinate line 349
32. abbrev OAI.Lech.RootChartAtlas.w line 350
33. lemma OAI.Lech.RootChartAtlas.coord_selected line 358
34. abbrev OAI.Lech.RootChartAtlas.fromH_R line 363
35. def OAI.Lech.RootChartAtlas.fromH line 372
36. lemma OAI.Lech.RootChartAtlas.fromH_source line 380
37. lemma OAI.Lech.RootChartAtlas.fromH_a line 390
38. lemma OAI.Lech.RootChartAtlas.fromH_b line 394
39. lemma OAI.Lech.RootChartAtlas.source_selected line 399
40. def OAI.Lech.RootChartAtlas.toH line 407
41. lemma OAI.Lech.RootChartAtlas.toH_coordinate line 415
42. lemma OAI.Lech.RootChartAtlas.fromH_toH line 421
43. lemma OAI.Lech.RootChartAtlas.fromH_X line 438
44. lemma OAI.Lech.RootChartAtlas.toH_fromH line 446
45. def OAI.Lech.RootChartAtlas.equiv line 464