OAI/NumberTheory/SingleFold/DescentMap.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SingleFold.Descent.E line 10
  2. instance OAI.SingleFold.Descent.(instance at line 11) line 11
  3. lemma OAI.SingleFold.Descent.equation line 16
  4. lemma OAI.SingleFold.Descent.negY line 19
  5. def OAI.SingleFold.Descent.adjusted line 21
  6. lemma OAI.SingleFold.Descent.adjusted_triple line 23
  7. lemma OAI.SingleFold.Descent.distinct_pair line 47
  8. lemma OAI.SingleFold.Descent.shifted_line line 55
  9. def OAI.SingleFold.Descent.alphaVal line 68
  10. lemma OAI.SingleFold.Descent.alphaVal_zero line 72
  11. lemma OAI.SingleFold.Descent.alphaVal_some line 73
  12. lemma OAI.SingleFold.Descent.alphaVal_ne_zero line 76
  13. lemma OAI.SingleFold.Descent.alphaVal_neg line 82
  14. lemma OAI.SingleFold.Descent.alphaVal_add_square line 87
  15. abbrev OAI.SingleFold.Descent.Squares line 142
  16. abbrev OAI.SingleFold.Descent.SquareClass line 143
  17. def OAI.SingleFold.Descent.classOf line 145
  18. lemma OAI.SingleFold.Descent.classOf_zero line 148
  19. lemma OAI.SingleFold.Descent.classOf_one line 149
  20. lemma OAI.SingleFold.Descent.classOf_mul line 151
  21. lemma OAI.SingleFold.Descent.classOf_eq_one_iff line 157
  22. lemma OAI.SingleFold.Descent.classOf_square line 171
  23. lemma OAI.SingleFold.Descent.classOf_self_mul line 176
  24. lemma OAI.SingleFold.Descent.squareClass_self_mul line 181
  25. lemma OAI.SingleFold.Descent.squareClass_inv line 192
  26. lemma OAI.SingleFold.Descent.classOf_inv line 195
  27. lemma OAI.SingleFold.Descent.classOf_div line 203
  28. lemma OAI.SingleFold.Descent.classOf_pow line 207
  29. def OAI.SingleFold.Descent.alpha line 215
  30. lemma OAI.SingleFold.Descent.half_algebra line 231
  31. lemma OAI.SingleFold.Descent.exists_half_of_squares line 267
  32. lemma OAI.SingleFold.Descent.not_isSquare_prime line 304
  33. def OAI.SingleFold.Descent.kummer line 311
  34. lemma OAI.SingleFold.Descent.kummer_halves line 314
  35. theorem OAI.SingleFold.Descent.kummer_eq_zero_iff line 319