OAI/RingTheory/Multiplicity/GradedLineBasisHasBasis.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Lech.GradedLineBasis.HasBasis line 29
  2. lemma OAI.Lech.GradedLineBasis.zero line 32
  3. lemma OAI.Lech.GradedLineBasis.add line 35
  4. def OAI.Lech.GradedLineBasis.cast line 43
  5. lemma OAI.Lech.GradedLineBasis.val_cast line 45
  6. lemma OAI.Lech.GradedLineBasis.val_unit line 48
  7. lemma OAI.Lech.GradedLineBasis.neg line 56
  8. def OAI.Lech.GradedLineBasis.subgroup line 78
  9. lemma OAI.Lech.GradedLineBasis.all_weights line 86
  10. lemma OAI.Lech.TensorBilinearValues.ext_mul line 113
  11. lemma OAI.Lech.TensorBilinearValues.ext_mul_equiv line 124
  12. abbrev OAI.Lech.RootInvariants.chartExtension line 144
  13. def OAI.Lech.RootInvariants.chartValue line 146
  14. lemma OAI.Lech.RootInvariants.chartValue_tmul line 149
  15. def OAI.Lech.RootInvariants.zeroLineEquiv line 154
  16. def OAI.Lech.RootInvariants.chartZeroEquiv line 172
  17. lemma OAI.Lech.RootInvariants.chartZero_value line 178
  18. def OAI.Lech.RootInvariants.chartMul line 183
  19. lemma OAI.Lech.RootInvariants.chartMul_tmul line 190
  20. lemma OAI.Lech.RootInvariants.chartValue_mul_tmul line 199
  21. lemma OAI.Lech.RootInvariants.chartValue_mul line 208
  22. def OAI.Lech.RootInvariants.chartSelectedUnit line 228
  23. lemma OAI.Lech.RootInvariants.chartSelectedUnit_val line 231
  24. def OAI.Lech.RootInvariants.chartWeight line 235
  25. lemma OAI.Lech.RootInvariants.chartWeight_zero line 239
  26. lemma OAI.Lech.RootInvariants.chartWeight_add line 242
  27. lemma OAI.Lech.RootInvariants.chartWeight_single line 246
  28. lemma OAI.Lech.RootInvariants.chart_all_weights line 253
  29. def OAI.Lech.LineBasisExtension.extend line 276
  30. def OAI.Lech.LineBasisExtension.coefficients line 282
  31. lemma OAI.Lech.LineBasisExtension.coefficients_tmul line 284
  32. lemma OAI.Lech.LineBasisExtension.value_extend line 287
  33. def OAI.Lech.LineBasisExtension.transition line 298
  34. lemma OAI.Lech.LineBasisExtension.transition_apply line 311
  35. lemma OAI.Lech.LineBasisExtension.transition_self line 315
  36. lemma OAI.Lech.LineBasisExtension.transition_cocycle line 318
  37. def OAI.Lech.RootInvariants.chartBasis line 340
  38. lemma OAI.Lech.RootInvariants.chartBasis_value line 343
  39. abbrev OAI.Lech.RootInvariants.commonModule line 349
  40. abbrev OAI.Lech.RootInvariants.commonExtension line 350
  41. def OAI.Lech.RootInvariants.commonBasis line 352
  42. def OAI.Lech.RootInvariants.commonCoefficients line 362
  43. def OAI.Lech.RootInvariants.commonWeight line 366
  44. def OAI.Lech.RootInvariants.commonValue line 370
  45. lemma OAI.Lech.RootInvariants.commonBasis_value line 372
  46. def OAI.Lech.RootInvariants.chartTransition line 390
  47. lemma OAI.Lech.RootInvariants.chartTransition_value line 395
  48. lemma OAI.Lech.RootInvariants.chartTransition_cocycle line 412
  49. lemma OAI.Lech.RootInvariants.commonWeight_single line 435
  50. lemma OAI.Lech.RootInvariants.commonCoordinate_relation line 443
  51. lemma OAI.Lech.RootInvariants.chartTransition_single line 459