OAI/Algebra/Drinfeld/Lattice.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DeligneDrinfeld.LatticeDimension.reduction_lift line 13
  2. theorem OAI.DeligneDrinfeld.LatticeDimension.reduction_lift_two line 34
  3. theorem OAI.DeligneDrinfeld.LatticeDimension.reduction_mono line 39
  4. abbrev OAI.DeligneDrinfeld.SaturatedSolutions.K line 53
  5. def OAI.DeligneDrinfeld.SaturatedSolutions.image line 56
  6. theorem OAI.DeligneDrinfeld.SaturatedSolutions.image_le line 58
  7. def OAI.DeligneDrinfeld.SaturatedSolutions.reduction line 62
  8. theorem OAI.DeligneDrinfeld.SaturatedSolutions.reduction_image_le line 65
  9. def OAI.DeligneDrinfeld.SaturatedSolutions.coordReduction line 69
  10. theorem OAI.DeligneDrinfeld.SaturatedSolutions.coordReduction_injective line 72
  11. theorem OAI.DeligneDrinfeld.SaturatedSolutions.coordReduction_surjective line 78
  12. theorem OAI.DeligneDrinfeld.SaturatedSolutions.finrank_reduction line 87
  13. def OAI.DeligneDrinfeld.SaturatedSolutions.filtration line 101
  14. def OAI.DeligneDrinfeld.SaturatedSolutions.inclusionFiltration line 104
  15. def OAI.DeligneDrinfeld.SaturatedSolutions.gradedMap line 108
  16. theorem OAI.DeligneDrinfeld.SaturatedSolutions.graded_kernel line 111
  17. theorem OAI.DeligneDrinfeld.SaturatedSolutions.filtration_zero line 115
  18. theorem OAI.DeligneDrinfeld.SaturatedSolutions.filtration_terminal line 119
  19. theorem OAI.DeligneDrinfeld.SaturatedSolutions.graded_surjective line 124
  20. theorem OAI.DeligneDrinfeld.SaturatedSolutions.lattice_lift line 134
  21. theorem OAI.DeligneDrinfeld.SaturatedSolutions.reduction_lift line 159
  22. theorem OAI.DeligneDrinfeld.LieGrading.eval_homogeneous line 182
  23. theorem OAI.DeligneDrinfeld.LieGrading.piece_tree line 186
  24. def OAI.DeligneDrinfeld.LieGrading.biTreeSpan line 190
  25. theorem OAI.DeligneDrinfeld.LieGrading.biTreeSpan_eq line 193
  26. theorem OAI.DeligneDrinfeld.LieGrading.treeDegree_pos line 218
  27. theorem OAI.DeligneDrinfeld.LieGrading.treeDegree_lower line 223
  28. theorem OAI.DeligneDrinfeld.LieGrading.leaf_degree_le line 228
  29. theorem OAI.DeligneDrinfeld.LieGrading.leaf_degree_lt line 241
  30. abbrev OAI.DeligneDrinfeld.NormalizedFamily.K line 263
  31. structure OAI.DeligneDrinfeld.NormalizedFamily.Data line 265
  32. def OAI.DeligneDrinfeld.NormalizedFamily.treeSolution line 277
  33. theorem OAI.DeligneDrinfeld.NormalizedFamily.treeWeight line 280
  34. def OAI.DeligneDrinfeld.NormalizedFamily.treeRep line 284
  35. theorem OAI.DeligneDrinfeld.NormalizedFamily.under_treeRep line 287
  36. theorem OAI.DeligneDrinfeld.NormalizedFamily.treeRep_leaf line 291
  37. theorem OAI.DeligneDrinfeld.NormalizedFamily.treeRep_node line 296
  38. theorem OAI.DeligneDrinfeld.NormalizedFamily.tree_leading line 302
  39. theorem OAI.DeligneDrinfeld.NormalizedFamily.bihomogeneous_leading line 328
  40. def OAI.DeligneDrinfeld.Triangular.assemble line 368
  41. theorem OAI.DeligneDrinfeld.Triangular.assemble_apply line 371
  42. theorem OAI.DeligneDrinfeld.Triangular.assemble_injective line 374
  43. def OAI.DeligneDrinfeld.NormalizedFamily.valueMap line 428
  44. def OAI.DeligneDrinfeld.NormalizedFamily.repMap line 432
  45. def OAI.DeligneDrinfeld.NormalizedFamily.leadingLinear line 435
  46. theorem OAI.DeligneDrinfeld.NormalizedFamily.leadingLinear_apply line 438
  47. theorem OAI.DeligneDrinfeld.NormalizedFamily.repMap_bihomogeneous line 441
  48. def OAI.DeligneDrinfeld.NormalizedFamily.oldPiece line 453
  49. theorem OAI.DeligneDrinfeld.NormalizedFamily.oldPiece_le line 456
  50. instance OAI.DeligneDrinfeld.NormalizedFamily.finite_oldPiece line 462
  51. def OAI.DeligneDrinfeld.NormalizedFamily.oldMap line 465
  52. def OAI.DeligneDrinfeld.NormalizedFamily.solutionLeading line 468
  53. theorem OAI.DeligneDrinfeld.NormalizedFamily.oldMap_leading line 471
  54. theorem OAI.DeligneDrinfeld.NormalizedFamily.oldMap_low line 484
  55. theorem OAI.DeligneDrinfeld.NormalizedFamily.old_assemble_injective line 490
  56. def OAI.DeligneDrinfeld.NormalizedFamily.fullMap line 520
  57. theorem OAI.DeligneDrinfeld.NormalizedFamily.fullMap_leading line 523
  58. theorem OAI.DeligneDrinfeld.NormalizedFamily.full_assemble_injective line 529
  59. theorem OAI.DeligneDrinfeld.NormalizedFamily.valueMap_injective line 547
  60. theorem OAI.DeligneDrinfeld.GenericIhara.cast_D line 574
  61. theorem OAI.DeligneDrinfeld.GenericIhara.cast_ihara line 587
  62. theorem OAI.DeligneDrinfeld.GenericIhara.cast_evalIhara line 591
  63. abbrev OAI.DeligneDrinfeld.IntegralFamily.K line 606
  64. structure OAI.DeligneDrinfeld.IntegralFamily.Values line 608
  65. structure OAI.DeligneDrinfeld.IntegralFamily.Family line 615
  66. def OAI.DeligneDrinfeld.IntegralFamily.cast line 622
  67. theorem OAI.DeligneDrinfeld.IntegralFamily.cast_homogeneous line 625
  68. theorem OAI.DeligneDrinfeld.IntegralFamily.rational_mem line 629
  69. theorem OAI.DeligneDrinfeld.IntegralFamily.eval_homogeneous line 637
  70. theorem OAI.DeligneDrinfeld.IntegralFamily.integral_eval_homogeneous line 643
  71. def OAI.DeligneDrinfeld.IntegralFamily.piece line 649
  72. theorem OAI.DeligneDrinfeld.IntegralFamily.integral_reduction_mem line 651
  73. theorem OAI.DeligneDrinfeld.IntegralFamily.tree_rational_W line 669
  74. theorem OAI.DeligneDrinfeld.IntegralFamily.reduced_solution line 674
  75. def OAI.DeligneDrinfeld.IntegralFamily.reducedValue line 692
  76. theorem OAI.DeligneDrinfeld.IntegralFamily.reduced_mem line 696