OAI/Algebra/FormalGroup/Honda/Tangent.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HeightThree.TangentClassification.expand_injective line 11
  2. lemma OAI.HeightThree.TangentClassification.pderiv_expand_zero line 17
  3. lemma OAI.HeightThree.TangentClassification.exists_expand_derivative_zero line 28
  4. lemma OAI.HeightThree.TangentClassification.exists_linear_add_expand line 47
  5. def OAI.HeightThree.TangentClassification.delta line 61
  6. lemma OAI.HeightThree.TangentClassification.delta_sub line 64
  7. lemma OAI.HeightThree.TangentClassification.delta_add line 70
  8. lemma OAI.HeightThree.TangentClassification.delta_smul line 76
  9. lemma OAI.HeightThree.TangentClassification.delta_X line 81
  10. lemma OAI.HeightThree.TangentClassification.pderiv_delta line 85
  11. lemma OAI.HeightThree.TangentClassification.derivative_constant_of_delta_expand line 95
  12. lemma OAI.HeightThree.TangentClassification.subst_expand_outer line 122
  13. lemma OAI.HeightThree.TangentClassification.delta_expand line 129
  14. lemma OAI.HeightThree.TangentClassification.partial_of_nonlinear_expand line 140
  15. theorem OAI.HeightThree.TangentClassification.tangent_decomposition line 152