OAI/NumberTheory/SingleFold/Rank.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleFold.AbstractRank.doubleRange line 11
  2. def OAI.SingleFold.AbstractRank.doubleKernel line 13
  3. lemma OAI.SingleFold.AbstractRank.mem_doubleRange line 15
  4. lemma OAI.SingleFold.AbstractRank.mem_doubleKernel line 16
  5. lemma OAI.SingleFold.AbstractRank.index_le_of_cover line 18
  6. lemma OAI.SingleFold.AbstractRank.doubleRange_prod line 33
  7. lemma OAI.SingleFold.AbstractRank.doubleRange_pi line 42
  8. lemma OAI.SingleFold.AbstractRank.doubleRange_int line 55
  9. lemma OAI.SingleFold.AbstractRank.free_index line 58
  10. lemma OAI.SingleFold.AbstractRank.finite_index_eq_kernel line 62
  11. lemma OAI.SingleFold.AbstractRank.doubleRange_map line 67
  12. lemma OAI.SingleFold.AbstractRank.doubleRange_index_equiv line 80
  13. def OAI.SingleFold.AbstractRank.doubleKernel_equiv line 85
  14. def OAI.SingleFold.AbstractRank.doubleKernel_free_prod_equiv line 102
  15. lemma OAI.SingleFold.AbstractRank.index_rank_formula line 118
  16. theorem OAI.SingleFold.AbstractRank.exists_rank_le_one line 127
  17. instance OAI.SingleFold.CurveRank.(instance at line 152) line 152
  18. def OAI.SingleFold.CurveRank.Tm5 line 166
  19. lemma OAI.SingleFold.CurveRank.double_torsion line 169
  20. lemma OAI.SingleFold.CurveRank.four_le_doubleKernel line 179
  21. theorem OAI.SingleFold.CurveRank.rank_at_most_one line 193
  22. abbrev OAI.SingleFold.ValuationRank.E line 206
  23. instance OAI.SingleFold.ValuationRank.(instance at line 207) line 207
  24. lemma OAI.SingleFold.ValuationRank.equation line 212
  25. lemma OAI.SingleFold.ValuationRank.val_add_eq line 215
  26. lemma OAI.SingleFold.ValuationRank.val_25 line 224
  27. lemma OAI.SingleFold.ValuationRank.val_4 line 228
  28. lemma OAI.SingleFold.ValuationRank.val_sq_add line 233
  29. lemma OAI.SingleFold.ValuationRank.val_sq_sub line 242
  30. lemma OAI.SingleFold.ValuationRank.duplication line 251
  31. lemma OAI.SingleFold.ValuationRank.double_val line 270
  32. def OAI.SingleFold.ValuationRank.vx line 291
  33. lemma OAI.SingleFold.ValuationRank.vx_double line 295
  34. def OAI.SingleFold.ValuationRank.G line 303
  35. lemma OAI.SingleFold.ValuationRank.vx_G line 306
  36. lemma OAI.SingleFold.ValuationRank.vx_dyadic line 311
  37. lemma OAI.SingleFold.ValuationRank.dyadic_injective line 319
  38. lemma OAI.SingleFold.ValuationRank.G_nontorsion line 325
  39. theorem OAI.SingleFold.CurveRank.rank_one line 336