OAI/RingTheory/FormalGroup/Endomorphism.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Coordinate endomorphisms of commutative formal groups and their natural action.

  1. structure OAI.LowerFormalGroup.End line 13
  2. def OAI.LowerFormalGroup.coordinate line 21
  3. def OAI.LowerFormalGroup.pSeries line 24
  4. def OAI.LowerFormalGroup.iterate line 27
  5. theorem OAI.LowerFormalGroup.const_subst line 31
  6. theorem OAI.LowerFormalGroup.order_subst_nonzero line 42
  7. theorem OAI.LowerFormalGroup.subst_ne_zero line 62
  8. def OAI.LowerFormalGroup.substPoint line 71
  9. theorem OAI.LowerFormalGroup.mixed_subst line 95
  10. theorem OAI.LowerFormalGroup.End.hasSubst line 103
  11. def OAI.LowerFormalGroup.End.action line 106
  12. theorem OAI.LowerFormalGroup.substPoint_coordinate line 156
  13. theorem OAI.LowerFormalGroup.End.action_coordinate line 162
  14. theorem OAI.LowerFormalGroup.End.action_commutes line 165
  15. def OAI.LowerFormalGroup.naturalEnd line 172
  16. def OAI.LowerFormalGroup.End.asNatural line 175
  17. theorem OAI.LowerFormalGroup.natural_apply line 180
  18. theorem OAI.LowerFormalGroup.natural_ext line 189
  19. def OAI.LowerFormalGroup.naturalSeries line 197
  20. theorem OAI.LowerFormalGroup.point_const_zero line 200
  21. theorem OAI.LowerFormalGroup.naturalSeries_injective line 204
  22. theorem OAI.LowerFormalGroup.naturalSeries_zero line 210
  23. theorem OAI.LowerFormalGroup.naturalSeries_one line 214
  24. theorem OAI.LowerFormalGroup.naturalSeries_asNatural line 218
  25. theorem OAI.LowerFormalGroup.naturalSeries_mul line 221
  26. theorem OAI.LowerFormalGroup.naturalSeries_eq_zero line 226
  27. theorem OAI.LowerFormalGroup.naturalSeries_constant_zero line 231
  28. theorem OAI.LowerFormalGroup.naturalSeries_pow_asNatural line 234
  29. theorem OAI.LowerFormalGroup.natural_mul_left_fixed line 241
  30. theorem OAI.LowerFormalGroup.natural_trace_zero line 257
  31. def OAI.LowerFormalGroup.pointGroup line 268
  32. def OAI.LowerFormalGroup.naturalRing line 287
  33. instance OAI.LowerFormalGroup.naturalNontrivial line 292
  34. instance OAI.LowerFormalGroup.naturalNoZeroDivisors line 298