OAI/RingTheory/Multiplicity/RootInvariantsWeightZero.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Lech.RootInvariants.weight_zero line 30
  2. lemma OAI.Lech.RootInvariants.linear_zero line 34
  3. def OAI.Lech.RootInvariants.algebra line 41
  4. lemma OAI.Lech.RootInvariants.algebra_toSubmodule line 45
  5. def OAI.Lech.RootInvariants.algebraModuleEquiv line 53
  6. lemma OAI.Lech.RootInvariants.algebra_finitePresentation line 56
  7. lemma OAI.Lech.RootInvariants.algebra_flat line 61
  8. lemma OAI.Lech.RootInvariants.algebra_rankAtStalk line 66
  9. def OAI.Lech.RootInvariants.algebraBaseMap line 72
  10. lemma OAI.Lech.RootInvariants.algebraBaseMap_linear line 76
  11. def OAI.Lech.RootInvariants.algebraTensorEquiv line 86
  12. def OAI.Lech.RootInvariants.algebraBaseMapRight line 108
  13. lemma OAI.Lech.RootInvariants.algebraBaseMapRight_eq line 112
  14. def OAI.Lech.RootInvariants.algebraTensorEquivRight line 117
  15. lemma OAI.Lech.RootInvariants.algebra_faithfullyFlat line 125
  16. def OAI.Lech.RootInvariants.overAlgebra line 143
  17. def OAI.Lech.RootInvariants.overAlgebraEquiv line 155
  18. def OAI.Lech.RootInvariants.lineBaseMap line 160
  19. def OAI.Lech.RootInvariants.lineBaseSourceEquiv line 165
  20. lemma OAI.Lech.RootInvariants.lineBaseSourceEquiv_symm_tmul line 176
  21. lemma OAI.Lech.RootInvariants.lineBaseMap_comp line 183
  22. def OAI.Lech.RootInvariants.lineTensorEquiv line 195
  23. lemma OAI.Lech.RootInvariants.weight_single line 223
  24. lemma OAI.Lech.RootInvariants.denominator_hom_root line 229
  25. def OAI.Lech.RootInvariants.sectionX line 237
  26. def OAI.Lech.RootInvariants.sectionY line 245
  27. lemma OAI.Lech.RootInvariants.section_chart_generator line 261
  28. lemma OAI.Lech.RootInvariants.leftUnit_eq line 279
  29. def OAI.Lech.RootInvariants.diagonalSection line 294
  30. lemma OAI.Lech.RootInvariants.diagonalSection_isUnit line 308
  31. lemma OAI.Lech.RootInvariants.sections_binary_form line 325
  32. def OAI.Lech.RootInvariants.selected line 361
  33. def OAI.Lech.RootInvariants.productSection line 366
  34. def OAI.Lech.RootInvariants.chartFunction line 383
  35. lemma OAI.Lech.RootInvariants.chartFunction_val line 396
  36. lemma OAI.Lech.RootInvariants.chartFunctions_span line 401