OAI/RingTheory/FormalGroup/Order.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Orders and linear coefficients of formal-group endomorphisms.

  1. lemma OAI.LowerFormalGroup.coeff_subst_zero_X line 11
  2. lemma OAI.LowerFormalGroup.formal_first_factor line 29
  3. lemma OAI.LowerFormalGroup.mv_const_subst line 51
  4. lemma OAI.LowerFormalGroup.points_hasSubst line 61
  5. lemma OAI.LowerFormalGroup.formal_point_factor line 69
  6. lemma OAI.LowerFormalGroup.formal_point_order line 84
  7. lemma OAI.LowerFormalGroup.formal_point_coeff_one line 93
  8. lemma OAI.LowerFormalGroup.coeff_one_subst line 100
  9. def OAI.LowerFormalGroup.naturalLinear line 113
  10. lemma OAI.LowerFormalGroup.naturalLinear_root_eq_one line 121
  11. lemma OAI.LowerFormalGroup.naturalSeries_order_one line 129
  12. lemma OAI.LowerFormalGroup.sum_powers_order_one line 139
  13. lemma OAI.LowerFormalGroup.naturalSeries_order_ne_zero line 149
  14. def OAI.LowerFormalGroup.naturalOrder line 153
  15. lemma OAI.LowerFormalGroup.naturalSeries_natCast line 165