OAI/RingTheory/FormalGroup/PrimeTorsion.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite-height constraints and coordinate expansions for endomorphisms of prime order.

  1. lemma OAI.LowerFormalGroup.formal_difference_order line 15
  2. lemma OAI.LowerFormalGroup.factor_power_order line 28
  3. lemma OAI.LowerFormalGroup.torsion_order_equation line 43
  4. lemma OAI.LowerFormalGroup.ordinary_difference_order line 70
  5. lemma OAI.LowerFormalGroup.ordinary_order_equation line 79
  6. lemma OAI.LowerFormalGroup.ordinary_power_order line 87
  7. lemma OAI.LowerFormalGroup.height_divisibility_and_order line 97
  8. theorem OAI.LowerFormalGroup.order_p_finite_height line 121
  9. lemma OAI.LowerFormalGroup.expansion_of_order line 148
  10. theorem OAI.LowerFormalGroup.order_p_finite_height_expansion line 174
  11. lemma OAI.LowerFormalGroup.iterate_inverse line 190