OAI/Algebra/FormalGroup/Honda/Evaluation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HeightThree.NilpotentEvaluation.constantHom line 11
  2. lemma OAI.HeightThree.NilpotentEvaluation.constantsHasSubst line 15
  3. def OAI.HeightThree.NilpotentEvaluation.eval line 19
  4. lemma OAI.HeightThree.NilpotentEvaluation.eval_X line 23
  5. lemma OAI.HeightThree.NilpotentEvaluation.eval_C line 28
  6. lemma OAI.HeightThree.NilpotentEvaluation.degree_two line 33
  7. lemma OAI.HeightThree.NilpotentEvaluation.tail_rect line 40
  8. lemma OAI.HeightThree.NilpotentEvaluation.hom_apply_eq_trunc line 67
  9. lemma OAI.HeightThree.NilpotentEvaluation.hom_ext_nilpotent line 75
  10. lemma OAI.HeightThree.NilpotentEvaluation.eval_natural line 97
  11. lemma OAI.HeightThree.NilpotentEvaluation.eval_zero line 104
  12. lemma OAI.HeightThree.NilpotentEvaluation.linear_coeff_mul_X line 115
  13. theorem OAI.HeightThree.NilpotentEvaluation.hom_difference_small line 126
  14. lemma OAI.HeightThree.NilpotentEvaluation.eval_augmentation line 193
  15. theorem OAI.HeightThree.NilpotentEvaluation.correct_parameters line 205