OAI/NumberTheory/SingleFold/LocalDescent.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleFold.LocalFive.mod_five_anisotropic line 7
  2. lemma OAI.SingleFold.LocalFive.five_dvd_of_sq line 18
  3. lemma OAI.SingleFold.LocalFive.no_norm_five_int line 21
  4. lemma OAI.SingleFold.LocalFive.no_norm_five line 41
  5. lemma OAI.SingleFold.LocalFive.no_norm_ten line 59
  6. lemma OAI.SingleFold.Descent.alpha_five_when_zero line 73
  7. def OAI.SingleFold.Descent.a0 line 124
  8. def OAI.SingleFold.Descent.a5 line 125
  9. def OAI.SingleFold.Descent.T0 line 127
  10. def OAI.SingleFold.Descent.T5 line 128
  11. def OAI.SingleFold.Descent.G line 129
  12. lemma OAI.SingleFold.Descent.a0_T0 line 131
  13. lemma OAI.SingleFold.Descent.a0_T5 line 136
  14. lemma OAI.SingleFold.Descent.a0_G line 139
  15. lemma OAI.SingleFold.Descent.a5_G line 144
  16. lemma OAI.SingleFold.Descent.normalize_a0 line 150
  17. theorem OAI.SingleFold.Descent.mod_two_cover line 170