OAI/Algebra/FormalGroup/Honda/PTypical.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HeightThree.PTypical.series line 11
  2. theorem OAI.HeightThree.PTypical.coeff_series_power line 14
  3. theorem OAI.HeightThree.PTypical.coeff_series_outside line 18
  4. theorem OAI.HeightThree.PTypical.series_constant line 22
  5. theorem OAI.HeightThree.PTypical.series_linear line 29
  6. def OAI.HeightThree.PTypical.HasIntegralNumerators line 33
  7. theorem OAI.HeightThree.PTypical.series_integralNumerators line 38
  8. def OAI.HeightThree.PTypical.IntegralSeries line 48
  9. def OAI.HeightThree.PTypical.integralLift line 51
  10. theorem OAI.HeightThree.PTypical.map_integralLift line 55
  11. theorem OAI.HeightThree.PTypical.integral_iff_range line 60
  12. theorem OAI.HeightThree.PTypical.power_difference line 69
  13. theorem OAI.HeightThree.PTypical.rational_cancel line 75
  14. theorem OAI.HeightThree.PTypical.logarithm_difference line 85
  15. lemma OAI.HeightThree.PTypical.constant_dvd_iff line 139
  16. theorem OAI.HeightThree.PTypical.frobenius_lift_series line 151
  17. def OAI.HeightThree.PTypical.twist line 178
  18. lemma OAI.HeightThree.PTypical.twist_coe line 182
  19. theorem OAI.HeightThree.PTypical.twist_iterate_congr line 185
  20. theorem OAI.HeightThree.PTypical.twist_iterate line 200
  21. theorem OAI.HeightThree.PTypical.twist_iterate_constant line 214
  22. theorem OAI.HeightThree.PTypical.map_twist_iterate line 219
  23. theorem OAI.HeightThree.PTypical.twist_iterate_subst line 233
  24. theorem OAI.HeightThree.PTypical.integralNumerators_map line 241
  25. theorem OAI.HeightThree.PTypical.integralNumerators_map_iterate line 257
  26. theorem OAI.HeightThree.PTypical.order_difference_powers line 267
  27. theorem OAI.HeightThree.PTypical.coeff_log_difference line 290
  28. theorem OAI.HeightThree.PTypical.order_log_difference line 310
  29. theorem OAI.HeightThree.PTypical.coeff_twist_iterate_zero line 319
  30. theorem OAI.HeightThree.PTypical.subst_twist_iterate line 336
  31. lemma OAI.HeightThree.PTypical.divide_p_mul line 345
  32. def OAI.HeightThree.PTypical.defect line 350
  33. lemma OAI.HeightThree.PTypical.defect_add line 354
  34. lemma OAI.HeightThree.PTypical.defect_sub line 360
  35. theorem OAI.HeightThree.PTypical.coeff_defect_le line 366
  36. theorem OAI.HeightThree.PTypical.defect_subst_eq line 379
  37. lemma OAI.HeightThree.PTypical.IntegralSeries.add line 403
  38. lemma OAI.HeightThree.PTypical.IntegralSeries.sub line 408
  39. lemma OAI.HeightThree.PTypical.integral_map line 413
  40. lemma OAI.HeightThree.PTypical.IntegralSeries.sum line 418
  41. theorem OAI.HeightThree.PTypical.defect_log_integral line 424
  42. theorem OAI.HeightThree.PTypical.integral_of_defect_log line 455