OAI/Algebra/FormalGroup/Honda/Transport.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HeightThree.CoordinateTransport.constantCoeff_pderiv line 11
  2. lemma OAI.HeightThree.CoordinateTransport.linear_subst line 15
  3. lemma OAI.HeightThree.CoordinateTransport.unilinear_subst line 23
  4. structure OAI.HeightThree.CoordinateTransport.Coordinate line 28
  5. def OAI.HeightThree.CoordinateTransport.Coordinate.ofSeries line 38
  6. def OAI.HeightThree.CoordinateTransport.Coordinate.symm line 46
  7. lemma OAI.HeightThree.CoordinateTransport.Coordinate.hasSubst line 48
  8. lemma OAI.HeightThree.CoordinateTransport.Coordinate.inv_hasSubst line 49
  9. lemma OAI.HeightThree.CoordinateTransport.Coordinate.series_const line 50
  10. lemma OAI.HeightThree.CoordinateTransport.Coordinate.inverse_const line 52
  11. lemma OAI.HeightThree.CoordinateTransport.Coordinate.series_inverse line 55
  12. lemma OAI.HeightThree.CoordinateTransport.Coordinate.inverse_series line 58
  13. lemma OAI.HeightThree.CoordinateTransport.Coordinate.inverse_injective line 61
  14. lemma OAI.HeightThree.CoordinateTransport.Coordinate.linear_inverse line 67
  15. def OAI.HeightThree.CoordinateTransport.Coordinate.law line 73
  16. lemma OAI.HeightThree.CoordinateTransport.Coordinate.formal_pair_const line 76
  17. lemma OAI.HeightThree.CoordinateTransport.Coordinate.law_const line 82
  18. lemma OAI.HeightThree.CoordinateTransport.Coordinate.law_pair line 85
  19. lemma OAI.HeightThree.CoordinateTransport.Coordinate.law_pair_const line 102
  20. lemma OAI.HeightThree.CoordinateTransport.Coordinate.inverse_law_pair line 108
  21. lemma OAI.HeightThree.CoordinateTransport.Coordinate.law_linear line 116
  22. def OAI.HeightThree.CoordinateTransport.Coordinate.transport line 126
  23. instance OAI.HeightThree.CoordinateTransport.Coordinate.transport_isComm line 142
  24. def OAI.HeightThree.CoordinateTransport.Coordinate.iso line 149
  25. def OAI.HeightThree.CoordinateTransport.Coordinate.map line 165
  26. lemma OAI.HeightThree.CoordinateTransport.Coordinate.transport_map line 183
  27. def OAI.HeightThree.CoordinateTransport.Coordinate.ofIso line 198
  28. lemma OAI.HeightThree.CoordinateTransport.Coordinate.transport_ofIso line 201
  29. lemma OAI.HeightThree.CoordinateTransport.Coordinate.map_eq_of_series_eq line 215
  30. def OAI.HeightThree.CoordinateTransport.Coordinate.ident line 226
  31. lemma OAI.HeightThree.CoordinateTransport.Coordinate.transport_ident line 229
  32. lemma OAI.HeightThree.CoordinateTransport.Coordinate.transport_map_eq_self line 238
  33. def OAI.HeightThree.CoordinateTransport.Coordinate.comp line 242
  34. def OAI.HeightThree.CoordinateTransport.CoordinateIso.refl line 261
  35. def OAI.HeightThree.CoordinateTransport.CoordinateIso.symm line 266
  36. lemma OAI.HeightThree.CoordinateTransport.CoordinateIso.trans_add line 288
  37. def OAI.HeightThree.CoordinateTransport.CoordinateIso.trans line 304
  38. def OAI.HeightThree.CoordinateTransport.CoordinateIso.map line 313
  39. lemma OAI.HeightThree.CoordinateTransport.unimap_comp line 336
  40. lemma OAI.HeightThree.CoordinateTransport.Coordinate.lift line 339
  41. lemma OAI.HeightThree.CoordinateTransport.formal_map_comp line 365
  42. lemma OAI.HeightThree.CoordinateTransport.formal_map_injective line 370