OAI/Algebra/FormalGroup/Honda/Cocycle.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HeightThree.HomogeneousCocycle.degree_pair line 11
  2. lemma OAI.HeightThree.HomogeneousCocycle.pair_exp line 15
  3. lemma OAI.HeightThree.HomogeneousCocycle.monomial_pair line 19
  4. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_sum line 26
  5. structure OAI.HeightThree.HomogeneousCocycle.IsCocycle line 57
  6. lemma OAI.HeightThree.HomogeneousCocycle.pair_subst_self line 66
  7. lemma OAI.HeightThree.HomogeneousCocycle.derivative_cocycle line 70
  8. lemma OAI.HeightThree.HomogeneousCocycle.derivative_monomial line 101
  9. lemma OAI.HeightThree.HomogeneousCocycle.subst_monomial_pair line 107
  10. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_derivative_axis line 116
  11. lemma OAI.HeightThree.HomogeneousCocycle.derivative_shape line 139
  12. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_of_coeff line 148
  13. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_sub line 156
  14. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_smul line 162
  15. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_X line 168
  16. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_one line 176
  17. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_pow line 184
  18. def OAI.HeightThree.HomogeneousCocycle.coboundary line 194
  19. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_coboundary line 196
  20. lemma OAI.HeightThree.HomogeneousCocycle.derivative_coboundary line 216
  21. lemma OAI.HeightThree.HomogeneousCocycle.coeff_add_pow line 222
  22. lemma OAI.HeightThree.HomogeneousCocycle.derivative_zero_support line 247
  23. lemma OAI.HeightThree.HomogeneousCocycle.derivative_symmetry line 268
  24. lemma OAI.HeightThree.HomogeneousCocycle.coboundary_symmetric line 277
  25. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_derivative_zero line 286
  26. lemma OAI.HeightThree.HomogeneousCocycle.coboundary_of_prime_not_dvd line 300
  27. lemma OAI.HeightThree.HomogeneousCocycle.choose_pred_cast line 326
  28. lemma OAI.HeightThree.HomogeneousCocycle.derivative_vanish_of_large_divisible line 344
  29. lemma OAI.HeightThree.HomogeneousCocycle.prime_power_sum line 373
  30. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_trace line 402
  31. lemma OAI.HeightThree.HomogeneousCocycle.derivative_vanish_at_prime line 432
  32. lemma OAI.HeightThree.HomogeneousCocycle.exists_expand_of_support line 471
  33. lemma OAI.HeightThree.HomogeneousCocycle.expand_injective line 491
  34. lemma OAI.HeightThree.HomogeneousCocycle.subst_expand line 497
  35. lemma OAI.HeightThree.HomogeneousCocycle.expand_subst_comm line 505
  36. lemma OAI.HeightThree.HomogeneousCocycle.isCocycle_of_expand line 517
  37. lemma OAI.HeightThree.HomogeneousCocycle.homogeneous_of_expand line 565
  38. lemma OAI.HeightThree.HomogeneousCocycle.expand_coboundary line 578
  39. theorem OAI.HeightThree.HomogeneousCocycle.cocycle_is_coboundary line 583