OAI/Algebra/FormalGroup/Honda/UniversalTransport.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HeightThree.UniversalTransport.transport_symm line 14
  2. lemma OAI.HeightThree.UniversalTransport.symm_transport line 18
  3. lemma OAI.HeightThree.UniversalTransport.coordinate_map_map line 22
  4. lemma OAI.HeightThree.UniversalTransport.coordinate_map_id line 27
  5. lemma OAI.HeightThree.UniversalTransport.coordinate_map_symm line 31
  6. lemma OAI.HeightThree.UniversalTransport.unimap_subst line 34
  7. lemma OAI.HeightThree.UniversalTransport.iso_trans_series line 38
  8. lemma OAI.HeightThree.UniversalTransport.iso_symm_series line 40
  9. lemma OAI.HeightThree.UniversalTransport.iso_series line 42
  10. lemma OAI.HeightThree.UniversalTransport.iso_inverse line 43
  11. lemma OAI.HeightThree.UniversalTransport.framed_transport line 45
  12. lemma OAI.HeightThree.UniversalTransport.framed_transport_iff line 56
  13. lemma OAI.HeightThree.UniversalTransport.scalar_coordinate_map line 64
  14. lemma OAI.HeightThree.UniversalTransport.scalar_coordinate_reduce line 71
  15. theorem OAI.HeightThree.UniversalTransport.isUniversal_transport line 83