OAI/Algebra/Drinfeld/Completion.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DeligneDrinfeld.LieGrading.weightSupport line 14
  2. theorem OAI.DeligneDrinfeld.LieGrading.piece_eq_zero_of_not_mem line 17
  3. theorem OAI.DeligneDrinfeld.LieGrading.sum_pieces line 35
  4. theorem OAI.DeligneDrinfeld.LieGrading.ext_pieces line 53
  5. theorem OAI.DeligneDrinfeld.PolynomialModuleCoefficients.eq_zero line 70
  6. theorem OAI.DeligneDrinfeld.PolynomialModuleCoefficients.mem line 86
  7. theorem OAI.DeligneDrinfeld.LieGrading.map_piece line 103
  8. theorem OAI.DeligneDrinfeld.LieGrading.injective_of_homogeneous line 117
  9. theorem OAI.DeligneDrinfeld.LieGrading.reflects_homogeneous line 126
  10. def OAI.DeligneDrinfeld.SolutionGrading.dilation line 140
  11. theorem OAI.DeligneDrinfeld.SolutionGrading.dilation_x line 141
  12. theorem OAI.DeligneDrinfeld.SolutionGrading.dilation_y line 142
  13. theorem OAI.DeligneDrinfeld.SolutionGrading.eval_dilation line 144
  14. def OAI.DeligneDrinfeld.SolutionGrading.braidDilation line 148
  15. theorem OAI.DeligneDrinfeld.SolutionGrading.braidDilation_t line 154
  16. theorem OAI.DeligneDrinfeld.SolutionGrading.dilation_W line 157
  17. theorem OAI.DeligneDrinfeld.SolutionGrading.dilation_homogeneous line 171
  18. theorem OAI.DeligneDrinfeld.SolutionGrading.dilation_sum line 185
  19. theorem OAI.DeligneDrinfeld.SolutionGrading.piece_W line 193
  20. theorem OAI.DeligneDrinfeld.SolutionGrading.piece_Wn line 204
  21. theorem OAI.DeligneDrinfeld.completed_leftInverse line 209
  22. theorem OAI.DeligneDrinfeld.completed_rightInverse line 217
  23. theorem OAI.DeligneDrinfeld.completed_continuous line 225
  24. theorem OAI.DeligneDrinfeld.completedInv_continuous line 233
  25. theorem OAI.DeligneDrinfeld.completed_bracket line 242
  26. instance OAI.DeligneDrinfeld.GradedGeneration.finite_Fn line 253
  27. theorem OAI.DeligneDrinfeld.GradedGeneration.Fn_eq_bot line 258
  28. theorem OAI.DeligneDrinfeld.GradedGeneration.homogeneous line 270
  29. def OAI.DeligneDrinfeld.GradedGeneration.valuePiece line 285
  30. theorem OAI.DeligneDrinfeld.GradedGeneration.valuePiece_injective line 292
  31. theorem OAI.DeligneDrinfeld.GradedGeneration.values_injective line 301
  32. theorem OAI.DeligneDrinfeld.GradedGeneration.valuePiece_surjective line 311
  33. def OAI.DeligneDrinfeld.GradedGeneration.valueMap line 325
  34. theorem OAI.DeligneDrinfeld.GradedGeneration.valueMap_bijective line 327
  35. def OAI.DeligneDrinfeld.GradedGeneration.equivalence line 349
  36. theorem OAI.DeligneDrinfeld.GradedGeneration.equivalence_graded line 351
  37. theorem OAI.DeligneDrinfeld.GradedGeneration.main_of_values line 370
  38. def OAI.DeligneDrinfeld.IntegralFamily.rangeValues line 387
  39. def OAI.DeligneDrinfeld.IntegralFamily.rangeFamily line 394
  40. def OAI.DeligneDrinfeld.IntegralFamily.rangePiece line 399
  41. theorem OAI.DeligneDrinfeld.IntegralFamily.rangePiece_surjective line 408
  42. theorem OAI.DeligneDrinfeld.IntegralFamily.range_dimension_lower line 426
  43. theorem OAI.DeligneDrinfeld.IntegralFamily.rangePiece_injective line 444
  44. theorem OAI.DeligneDrinfeld.IntegralFamily.main_of_normalized line 449
  45. theorem OAI.DeligneDrinfeld.IntegralFamily.main_of_oddValues line 473
  46. def OAI.DeligneDrinfeld.CategoricalValues.OddWitnesses line 480
  47. theorem OAI.DeligneDrinfeld.CategoricalValues.main_of_oddWitnesses line 484
  48. def OAI.DeligneDrinfeld.CategoricalValues.ofSolution line 492
  49. theorem OAI.DeligneDrinfeld.CategoricalValues.value_ofSolution line 508
  50. theorem OAI.DeligneDrinfeld.CategoricalValues.Wn_le_values line 511
  51. theorem OAI.DeligneDrinfeld.CategoricalValues.values_eq_W line 522
  52. theorem OAI.DeligneDrinfeld.CategoricalValues.W_ihara_closed line 531
  53. theorem OAI.DeligneDrinfeld.CategoricalValues.main_of_oddSolutions line 535
  54. theorem OAI.DeligneDrinfeld.real_odd_nonzero line 547
  55. theorem OAI.DeligneDrinfeld.odd_solution line 553
  56. theorem OAI.DeligneDrinfeld.main line 559

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: OAI.DeligneDrinfeld.MainStatement

    Proof uses: OAI.DeligneDrinfeld.CategoricalValues.main_of_oddSolutions, OAI.DeligneDrinfeld.odd_solution

    Distinct definitions of this name: ComparatorChallenges/DeligneDrinfeld.lean:189 (same statement text; different proof or body). Qualify references as OAI.DeligneDrinfeld.main@path.