OAI/RingTheory/Multiplicity/RootBundleChartsDenominator.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.RootBundleCharts.denominator line 26
  2. lemma OAI.Lech.RootBundleCharts.denominator_val line 28
  3. lemma OAI.Lech.RootBundleCharts.hom_denominator line 32
  4. def OAI.Lech.RootBundleCharts.weight line 47
  5. lemma OAI.Lech.RootBundleCharts.weight_cocycle line 50
  6. def OAI.Lech.RootBundleCharts.transition line 61
  7. lemma OAI.Lech.RootBundleCharts.transition_apply line 65
  8. lemma OAI.Lech.RootBundleCharts.transition_cocycle line 70
  9. lemma OAI.Lech.RootBundleCharts.hom_identity line 89
  10. lemma OAI.Lech.RootBundleCharts.denominator_identity line 95
  11. lemma OAI.Lech.RootBundleCharts.weight_identity line 100
  12. lemma OAI.Lech.RootBundleCharts.transition_identity line 103
  13. lemma OAI.Lech.RootBundleCharts.factor_coordinates line 110
  14. def OAI.Lech.RootBundleCharts.chartBasis line 127
  15. lemma OAI.Lech.RootBaseChange.mapped_eval line 147
  16. lemma OAI.Lech.RootBaseChange.chartFactorization line 153
  17. def OAI.Lech.RootBaseChange.chartMap line 161
  18. lemma OAI.Lech.RootBaseChange.chartMap_root line 164
  19. lemma OAI.Lech.RootBaseChange.chartMap_denominator line 167
  20. lemma OAI.Lech.RootBaseChange.chartMap_weight line 179
  21. def OAI.Lech.RootBaseChange.baseHom line 188
  22. def OAI.Lech.RootBaseChange.baseTransition line 195
  23. lemma OAI.Lech.RootBaseChange.chartMap_hom line 203
  24. lemma OAI.Lech.RootBaseChange.transition_natural line 219
  25. def OAI.Lech.UniversalSplitting.Data.canonicalHom line 241
  26. lemma OAI.Lech.UniversalSplitting.Data.canonicalHom_root line 244
  27. lemma OAI.Lech.UniversalSplitting.Data.canonicalHom_comp line 248
  28. lemma OAI.Lech.UniversalSplitting.Data.canonicalHom_self line 254
  29. def OAI.Lech.UniversalSplitting.Data.canonicalEquiv line 259
  30. lemma OAI.Lech.UniversalSplitting.Data.canonicalEquiv_root line 264
  31. def OAI.Lech.UniversalSplitting.Data.baseChangeEquiv line 268
  32. lemma OAI.Lech.UniversalSplitting.Data.baseChangeEquiv_root line 273
  33. def OAI.Lech.UniversalSplitting.Data.baseChangeEquivOfMap line 285
  34. lemma OAI.Lech.UniversalSplitting.Data.baseChangeEquivOfMap_root line 291
  35. def OAI.Lech.RootBaseChange.chartTensorEquiv line 317
  36. lemma OAI.Lech.RootBaseChange.chartTensorEquiv_root line 321
  37. lemma OAI.Lech.RootBaseChange.chartTensorEquiv_includeRight line 325
  38. lemma OAI.Lech.RootBaseChange.chartTensorEquiv_tmul line 332
  39. lemma OAI.Lech.RootBaseChange.tensor_transition line 345
  40. lemma OAI.Lech.RootTransport.mapped_eval line 372
  41. lemma OAI.Lech.RootTransport.shift_factorization line 378
  42. def OAI.Lech.RootTransport.hom line 386
  43. lemma OAI.Lech.RootTransport.hom_root line 390
  44. lemma OAI.Lech.RootTransport.denominator_unit line 395
  45. def OAI.Lech.RootTransport.denominator line 399
  46. lemma OAI.Lech.RootTransport.denominator_val line 402
  47. def OAI.Lech.RootTransport.weight line 406
  48. def OAI.Lech.RootTransport.linear line 409
  49. lemma OAI.Lech.RootTransport.linear_apply line 413