OAI/Algebra/FormalGroup/Honda/Universality.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.HeightThree.ArtinianUniversality.mapFormalGroup_isComm line 13
  2. lemma OAI.HeightThree.ArtinianUniversality.framed_refl line 24
  3. lemma OAI.HeightThree.ArtinianUniversality.framed_symm line 38
  4. lemma OAI.HeightThree.ArtinianUniversality.framed_trans line 45
  5. lemma OAI.HeightThree.ArtinianUniversality.framed_map line 55
  6. lemma OAI.HeightThree.ArtinianUniversality.augmentation_of_base_map line 63
  7. lemma OAI.HeightThree.ArtinianUniversality.lift_base_map line 68
  8. structure OAI.HeightThree.ArtinianUniversality.Data line 91
  9. instance OAI.HeightThree.ArtinianUniversality.Data.family_isComm line 106
  10. lemma OAI.HeightThree.ArtinianUniversality.Data.multiply_coeff_map line 108
  11. lemma OAI.HeightThree.ArtinianUniversality.Data.base_gamma line 112
  12. lemma OAI.HeightThree.ArtinianUniversality.Data.gamma_honda line 120
  13. lemma OAI.HeightThree.ArtinianUniversality.Data.gamma_nonlinear line 124
  14. lemma OAI.HeightThree.ArtinianUniversality.Data.gamma_frobenius line 130
  15. lemma OAI.HeightThree.ArtinianUniversality.Data.lift_step line 139
  16. lemma OAI.HeightThree.ArtinianUniversality.Data.existence line 197
  17. lemma OAI.HeightThree.ArtinianUniversality.Data.family_honda line 227
  18. lemma OAI.HeightThree.ArtinianRigidity.equivalence_rigid line 237
  19. lemma OAI.HeightThree.ArtinianUniversality.Data.base_map_unique line 252
  20. theorem OAI.HeightThree.ArtinianUniversality.Data.isUniversal line 318