OAI/Geometry/QuadricBundles/Graphs.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.QuadricCounterexample.GraphScalars line 11
  2. def OAI.QuadricCounterexample.GraphScalars.N₁ line 25
  3. def OAI.QuadricCounterexample.GraphScalars.N₂ line 26
  4. def OAI.QuadricCounterexample.GraphScalars.N₂other line 27
  5. def OAI.QuadricCounterexample.GraphScalars.P₁ line 28
  6. def OAI.QuadricCounterexample.GraphScalars.P₂ line 29
  7. def OAI.QuadricCounterexample.GraphScalars.L line 30
  8. def OAI.QuadricCounterexample.GraphScalars.J line 31
  9. lemma OAI.QuadricCounterexample.GraphScalars.a_twentyfour line 33
  10. lemma OAI.QuadricCounterexample.GraphScalars.sqrt_two_square line 36
  11. lemma OAI.QuadricCounterexample.GraphScalars.N₁_dvd line 40
  12. lemma OAI.QuadricCounterexample.GraphScalars.N₂_factor line 46
  13. lemma OAI.QuadricCounterexample.GraphScalars.N₂_dvd line 53
  14. lemma OAI.QuadricCounterexample.GraphScalars.N_coprime line 63
  15. lemma OAI.QuadricCounterexample.GraphScalars.exists_N_quotient line 79
  16. def OAI.QuadricCounterexample.GraphScalars.Nquotient line 82
  17. lemma OAI.QuadricCounterexample.GraphScalars.Nquotient_spec line 83
  18. lemma OAI.QuadricCounterexample.GraphScalars.N₁_comp_L line 85
  19. lemma OAI.QuadricCounterexample.GraphScalars.N₂_comp_L line 93
  20. lemma OAI.QuadricCounterexample.GraphScalars.P_coprime line 102
  21. lemma OAI.QuadricCounterexample.GraphScalars.P_product_dvd line 110
  22. lemma OAI.QuadricCounterexample.GraphScalars.J_mod_P₁ line 117
  23. lemma OAI.QuadricCounterexample.GraphScalars.J_mod_P₂ line 122
  24. lemma OAI.QuadricCounterexample.GraphScalars.P₁_dvd_mixed line 127
  25. lemma OAI.QuadricCounterexample.GraphScalars.P₂_dvd_mixed line 136
  26. lemma OAI.QuadricCounterexample.GraphScalars.exists_graph_quotients line 148
  27. def OAI.QuadricCounterexample.GraphScalars.sameQuotient line 154
  28. def OAI.QuadricCounterexample.GraphScalars.mixedQuotient line 155
  29. lemma OAI.QuadricCounterexample.GraphScalars.sameQuotient_spec line 156
  30. lemma OAI.QuadricCounterexample.GraphScalars.mixedQuotient_spec line 158
  31. def OAI.QuadricCounterexample.GraphScalars.graphOne line 161
  32. def OAI.QuadricCounterexample.GraphScalars.graphTwo line 162
  33. def OAI.QuadricCounterexample.GraphScalars.graphThree line 163
  34. def OAI.QuadricCounterexample.GraphScalars.betaPolynomial line 165
  35. def OAI.QuadricCounterexample.GraphScalars.liftBeta line 167
  36. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_one line 172
  37. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_two line 175
  38. lemma OAI.QuadricCounterexample.GraphScalars.eval_P₁_same line 179
  39. lemma OAI.QuadricCounterexample.GraphScalars.eval_P₂_same line 186
  40. lemma OAI.QuadricCounterexample.GraphScalars.eval_P₁_mixed line 193
  41. lemma OAI.QuadricCounterexample.GraphScalars.eval_P₂_mixed line 199
  42. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_three line 205
  43. lemma OAI.QuadricCounterexample.GraphScalars.betaPolynomial_ne_zero line 217
  44. lemma OAI.QuadricCounterexample.GraphScalars.a_ne_zero line 238
  45. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_ne_zero line 244
  46. abbrev OAI.QuadricCounterexample.BPoly line 272
  47. def OAI.QuadricCounterexample.affineLinear line 274
  48. lemma OAI.QuadricCounterexample.affineLinear_regular_variable line 276
  49. lemma OAI.QuadricCounterexample.affineLinear_ne_zero_of_left line 285
  50. lemma OAI.QuadricCounterexample.affineLinear_ne_zero_of_right line 293
  51. lemma OAI.QuadricCounterexample.determinant_graph_irreducible line 298
  52. def OAI.QuadricCounterexample.GraphScalars.G1 line 323
  53. def OAI.QuadricCounterexample.GraphScalars.G2 line 324
  54. def OAI.QuadricCounterexample.GraphScalars.G3 line 325
  55. lemma OAI.QuadricCounterexample.GraphScalars.eval_G1 line 329
  56. lemma OAI.QuadricCounterexample.GraphScalars.eval_G2 line 332
  57. lemma OAI.QuadricCounterexample.GraphScalars.eval_G3 line 335
  58. lemma OAI.QuadricCounterexample.GraphScalars.G1_irreducible line 339
  59. lemma OAI.QuadricCounterexample.GraphScalars.G2_irreducible line 346
  60. lemma OAI.QuadricCounterexample.GraphScalars.G3_irreducible line 355
  61. lemma OAI.QuadricCounterexample.GraphScalars.a_square_ne_one line 369
  62. lemma OAI.QuadricCounterexample.GraphScalars.G1_G2_relPrime line 378
  63. lemma OAI.QuadricCounterexample.GraphScalars.G1_G3_relPrime line 388
  64. lemma OAI.QuadricCounterexample.GraphScalars.G2_G3_relPrime line 401
  65. lemma OAI.QuadricCounterexample.GraphScalars.graphProduct_squarefree line 415
  66. lemma OAI.QuadricCounterexample.GraphScalars.graphProduct_dvd_of_eval_zero line 422
  67. def OAI.QuadricCounterexample.source_a line 446
  68. def OAI.QuadricCounterexample.source_s line 447
  69. def OAI.QuadricCounterexample.source_A line 449
  70. def OAI.QuadricCounterexample.source_B line 450
  71. lemma OAI.QuadricCounterexample.source_a_eq line 453
  72. lemma OAI.QuadricCounterexample.sqrt_two_sq_complex line 462
  73. lemma OAI.QuadricCounterexample.sqrt_three_sq_complex line 466
  74. lemma OAI.QuadricCounterexample.sqrt_three_ne_zero_complex line 470
  75. lemma OAI.QuadricCounterexample.source_a_inv_eq line 473
  76. lemma OAI.QuadricCounterexample.source_a_add_inv line 482
  77. lemma OAI.QuadricCounterexample.source_a_ne_zero line 486
  78. lemma OAI.QuadricCounterexample.source_a_mul_inv line 488
  79. lemma OAI.QuadricCounterexample.source_s_mul_complement line 490
  80. lemma OAI.QuadricCounterexample.source_a_square line 501
  81. lemma OAI.QuadricCounterexample.source_a_cube line 506
  82. lemma OAI.QuadricCounterexample.source_a_twentyfour line 509
  83. lemma OAI.QuadricCounterexample.source_graph_trace line 519
  84. def OAI.QuadricCounterexample.sourceGraphScalars line 531
  85. def OAI.QuadricCounterexample.GraphScalars.swapped line 546
  86. lemma OAI.QuadricCounterexample.GraphScalars.swapped_swapped line 560
  87. def OAI.QuadricCounterexample.affineRepresentative line 572
  88. lemma OAI.QuadricCounterexample.affineRepresentative_index line 575
  89. lemma OAI.QuadricCounterexample.affineRepresentative_change line 579
  90. def OAI.QuadricCounterexample.matrixGraphValue line 587
  91. def OAI.QuadricCounterexample.matrixGraphPolynomial line 592
  92. lemma OAI.QuadricCounterexample.baseEval_matrixGraphPolynomial line 597
  93. lemma OAI.QuadricCounterexample.matrixGraphValue_change line 603
  94. def OAI.QuadricCounterexample.matrixBranchDenominator line 616
  95. lemma OAI.QuadricCounterexample.matrixGraphValue_zero_iff line 619
  96. lemma OAI.QuadricCounterexample.matrixBranchDenominator_change line 638
  97. def OAI.QuadricCounterexample.GraphScalars.matrices line 654
  98. def OAI.QuadricCounterexample.GraphScalars.chartScalars line 657
  99. def OAI.QuadricCounterexample.GraphScalars.mixedChart line 659
  100. def OAI.QuadricCounterexample.GraphScalars.chartProduct line 661
  101. def OAI.QuadricCounterexample.GraphScalars.divisorPolynomial line 664
  102. def OAI.QuadricCounterexample.GraphScalars.chartUnit line 668
  103. lemma OAI.QuadricCounterexample.GraphScalars.chartUnit_ne_zero line 670
  104. lemma OAI.QuadricCounterexample.GraphScalars.divisorPolynomial_eq line 674
  105. lemma OAI.QuadricCounterexample.GraphScalars.divisorPolynomial_reduced line 686
  106. lemma OAI.QuadricCounterexample.GraphScalars.divisorPolynomial_nonzero line 694
  107. lemma OAI.QuadricCounterexample.GraphScalars.divisorPolynomial_change line 697
  108. def OAI.QuadricCounterexample.GraphScalars.branchGraph line 716
  109. def OAI.QuadricCounterexample.GraphScalars.branchDenominator line 719
  110. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_branch_one line 724
  111. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_branch_two line 734
  112. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_branch_three line 748
  113. lemma OAI.QuadricCounterexample.GraphScalars.liftBeta_branch line 767
  114. lemma OAI.QuadricCounterexample.GraphScalars.baseEval_pow line 775
  115. def OAI.QuadricCounterexample.GraphScalars.liftPolynomial line 778
  116. lemma OAI.QuadricCounterexample.GraphScalars.eval_aeval_snd line 783
  117. lemma OAI.QuadricCounterexample.GraphScalars.eval_liftPolynomial line 789
  118. def OAI.QuadricCounterexample.GraphScalars.chartLift line 795
  119. lemma OAI.QuadricCounterexample.GraphScalars.eval_chartLift line 798
  120. lemma OAI.QuadricCounterexample.GraphScalars.matrixGraphValue_eq_branch line 802
  121. lemma OAI.QuadricCounterexample.GraphScalars.matrixBranchDenominator_eq line 813
  122. lemma OAI.QuadricCounterexample.GraphScalars.chartLift_branch line 821
  123. lemma OAI.QuadricCounterexample.GraphScalars.divisor_zero_branch line 834
  124. lemma OAI.QuadricCounterexample.GraphScalars.chartLift_unit line 843
  125. lemma OAI.QuadricCounterexample.GraphScalars.chartLift_change line 848
  126. def OAI.QuadricCounterexample.GraphScalars.equalizerData line 873
  127. def OAI.QuadricCounterexample.sourceBundle line 884